diff options
author | 2016-09-30 09:46:54 +0200 | |
---|---|---|
committer | 2016-09-30 09:46:54 +0200 | |
commit | 916d5fcc32f5110f23b60b21489d89598e6b8674 (patch) | |
tree | 2b1d840fa7623d386a0321a380d9f76f03f93841 /test-suite/bugs/closed | |
parent | edb55a94fc5c0473e57f5a61c0c723194c2ff414 (diff) | |
parent | 7952c15ca3d26ae5c2807196bb7aca97bce325c6 (diff) |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/4762.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v new file mode 100644 index 000000000..7a87b07a8 --- /dev/null +++ b/test-suite/bugs/closed/4762.v @@ -0,0 +1,24 @@ +Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q. + +Lemma foo P Q R : R = myand P Q -> P -> Q -> R. +Proof. intros ->; constructor; auto. Qed. + +Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test1. +Qed. + +Hint Extern 0 => + match goal with + | |- myand _ _ => eapply foo; [reflexivity| |] + end : test2. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test2. (* works *) +Qed. + |