diff options
| author | Maxime Dénès | 2016-09-30 09:14:41 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 09:14:41 +0200 |
| commit | 7952c15ca3d26ae5c2807196bb7aca97bce325c6 (patch) | |
| tree | f80c78d9851f9e43263cd9ee64c4669d2a599ee1 | |
| parent | 4e3d4646788c96f16193df14a81aa79938812194 (diff) | |
| parent | 844b076bf5150a107d31cd4648955c3a6538a34b (diff) | |
Merge branch '4762' into v8.5
Was PR#293: Fix #4762 (eauto weaker than auto).
| -rw-r--r-- | tactics/eauto.ml4 | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4762.v | 24 |
2 files changed, 26 insertions, 1 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index cb206a7dd1..7e37722e93 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -291,7 +291,8 @@ module SearchProblem = struct in let rec_tacs = let l = - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + let concl = Reductionops.nf_evar (project g)(pf_concl g) in + filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl) in List.map (fun (lgls, cost, pp) -> diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v new file mode 100644 index 0000000000..7a87b07a8e --- /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. + |