prettify: fix missed useless prefix annotation

artagnon · Feb 20, 2024 · 55e109b · 55e109b
1 parent 0042604
commit 55e109b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/νType/νType.v b/theories/νType/νType.v
@@ -147,7 +147,7 @@ Class PaintingBlock (n: nat) (prefix: Type@{m'})
   painting {p} {Hp: p <= n} {D}:
     (Frame.(frame) (♢ _) D -> HSet@{m}) -> Frame.(frame) Hp D -> HSet@{m};
   restrPainting {p q} {Hpq: p.+1 <= q.+1}
-    (Hq: q.+1 <= n) (ε: arity) {D : prefix}
+    (Hq: q.+1 <= n) (ε: arity) {D}
     {E: Frame.(frame) (♢ _) D -> HSet@{m}}
     {d: Frame.(frame) (↓ (Hpq ↕ Hq)) D} (c: painting E d):
     PaintingPrev.(painting') (Frame.(restrFrame) Hq ε d);