diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1704.v | 2 | ||||
| -rw-r--r-- | test-suite/typeclasses/unification_delta.v | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1704.v b/test-suite/bugs/closed/shouldsucceed/1704.v index 81b221690..4b02d5f93 100644 --- a/test-suite/bugs/closed/shouldsucceed/1704.v +++ b/test-suite/bugs/closed/shouldsucceed/1704.v @@ -12,6 +12,6 @@ Axiom r : False -> 0 == 1. Goal 0 == 0. Proof. rewrite r. -refl. +reflexivity. admit. Qed. diff --git a/test-suite/typeclasses/unification_delta.v b/test-suite/typeclasses/unification_delta.v index b8789f26e..663a837f3 100644 --- a/test-suite/typeclasses/unification_delta.v +++ b/test-suite/typeclasses/unification_delta.v @@ -7,15 +7,15 @@ Lemma bla : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y Proof. intros. rewrite H0. - refl. + reflexivity. Defined. Lemma bla' : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x. Proof. intros. - (* Need delta no [relation] to unify with the right lemmas. *) + (* Need delta on [relation] to unify with the right lemmas. *) rewrite <- H0. - refl. + reflexivity. Qed. Axiom euclid : nat -> { x : nat | x > 0 } -> nat. |