diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 17:43:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 17:44:34 +0200 |
| commit | 112e974ec90b2afc51a7cffeba49e5777f3ea80f (patch) | |
| tree | 1bf579fca94adea5ee4a423c0a96c8832e68861e /test-suite | |
| parent | 8b2a08ecd123515778584596918666e5f49076f7 (diff) | |
| parent | 6d55121c90ec50319a3de6a6907726fbcdc2f835 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4416.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4863.v | 32 |
2 files changed, 35 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v new file mode 100644 index 000000000..b97a8ce64 --- /dev/null +++ b/test-suite/bugs/closed/4416.v @@ -0,0 +1,3 @@ +Goal exists x, x. +unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end. +(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file 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*) |