diff options
Diffstat (limited to 'test-suite/bugs/closed/4863.v')
| -rw-r--r-- | test-suite/bugs/closed/4863.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v index e884355fd..1e47f2957 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. |