From 4e3d4646788c96f16193df14a81aa79938812194 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 29 Sep 2016 09:35:07 +0200 Subject: Fix a bug in subst releaved by an OCaml warning. --- tactics/equality.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 06a9b317a..b4c027382 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1730,20 +1730,22 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let test (hyp,_,c) = + let select_equation_name (hyp,_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with - | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> + | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> + Some hyp + | _, Var z when not (is_evaluable env (EvalVarRef z)) -> Some hyp | _ -> None with Constr_matching.PatternMatchingFailure -> None in let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter test hyps) + List.rev (List.map_filter select_equation_name hyps) in (* Second step: treat equations *) -- cgit v1.2.3 From 844b076bf5150a107d31cd4648955c3a6538a34b Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Wed, 28 Sep 2016 10:40:54 +0200 Subject: Fix #4762. --- tactics/eauto.ml4 | 3 ++- test-suite/bugs/closed/4762.v | 24 ++++++++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4762.v (limited to 'tactics') diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index cb206a7dd..7e37722e9 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 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. + -- cgit v1.2.3