diff options
| -rw-r--r-- | test-suite/success/Equations.v | 4 | ||||
| -rw-r--r-- | test-suite/success/Generalization.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v index 450345524..d3b53ba5d 100644 --- a/test-suite/success/Equations.v +++ b/test-suite/success/Equations.v @@ -94,7 +94,7 @@ below_nat P (S n) step := let rest := below_nat P n step in (step n rest, rest). Class BelowPack (A : Type) := - Below : Type ; below : Below. + { Below : Type ; below : Below }. Instance nat_BelowPack : BelowPack nat := Below := Π P n step, Below_nat P n ; @@ -126,7 +126,7 @@ Definition rec_vector (P : Π A n, vector A n -> Type) A n v step A n v (below_vector P A n v step). Class Recursor (A : Type) (BP : BelowPack A) := - rec_type : Π x : A, Type ; rec : Π x : A, rec_type x. + { rec_type : Π x : A, Type ; rec : Π x : A, rec_type x }. Instance nat_Recursor : Recursor nat nat_BelowPack := rec_type := λ n, Π P step, P n ; diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v index d86d34d35..6b503e95a 100644 --- a/test-suite/success/Generalization.v +++ b/test-suite/success/Generalization.v @@ -2,7 +2,7 @@ Check `(a = 0). Check `(a = 0)%type. Definition relation A := A -> A -> Prop. -Definition equivalence {(R : relation A)} := True. +Definition equivalence `(R : relation A) := True. Check (`(@equivalence A R)). Definition a_eq_b : `( a = 0 /\ a = b /\ b > c \/ d = e /\ d = 1). |