diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-06 18:02:25 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-11 11:17:10 +0200 |
| commit | b247761476c4b36f0945c19c23c171ea57701178 (patch) | |
| tree | 95733168d350fd3c014c1eb7f7792c6bc3d431f4 /test-suite | |
| parent | 009718d9d0130a967261ae5d2484985522fc2f7c (diff) | |
Fix for bug #4863, update the Proofview's env with
side_effects. Partial solution to the handling of side effects
in proofview.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4863.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v new file mode 100644 index 000000000..e884355fd --- /dev/null +++ b/test-suite/bugs/closed/4863.v @@ -0,0 +1,32 @@ +Require Import Classes.DecidableClass. + +Inductive Foo : Set := +| foo1 | foo2. + +Instance 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. + +Goal forall (a b : Foo), {a=b}+{a<>b}. +intros. +abstract (abstract (decide equality)). (*abstract works here*) +Qed. + +Check ltac:(abstract (exact I)) : True. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. typeclasses eauto. typeclasses eauto. Qed. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. +refine _. +refine _. +Defined. +(*fails*) |