diff options
| -rw-r--r-- | test-suite/bugs/closed/3699.v | 12 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4863.v | 7 | ||||
| -rw-r--r-- | test-suite/success/bteauto.v | 2 |
3 files changed, 9 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 8dadc2419c..efa4325264 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +46,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. @@ -111,8 +109,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +121,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v index e884355fde..1e47f2957b 100644 --- a/test-suite/bugs/closed/4863.v +++ b/test-suite/bugs/closed/4863.v @@ -3,14 +3,14 @@ Require Import Classes.DecidableClass. Inductive Foo : Set := | foo1 | foo2. -Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. +Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. Proof. intros P H. refine (Build_Decidable _ (if H then true else false) _). intuition congruence. Qed. -Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances. +Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances. Goal forall (a b : Foo), {a=b}+{a<>b}. intros. @@ -21,7 +21,8 @@ Check ltac:(abstract (exact I)) : True. Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). intros. -split. typeclasses eauto. typeclasses eauto. Qed. +split. typeclasses eauto. +typeclasses eauto. Qed. Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). intros. diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index f97f764b4d..3178c6fc15 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -1,3 +1,4 @@ +Require Import Program.Tactics. Module Backtracking. Class A := { foo : nat }. @@ -8,7 +9,6 @@ Module Backtracking. Qed. Arguments foo A : clear implicits. - Require Import Program.Tactics. Example find42 : exists n, n = 42. Proof. eexists. |