diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c5b87761d8..591fbabaef 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1667,17 +1667,18 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* First step: find hypotheses to treat in linear time *) let find_equations gl = 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) = 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; - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if Term.eq_constr x y then None else match kind_of_term x, kind_of_term y with - | Var _, _ | _, Var _ -> Some hyp - | _ -> None + | Var z, _ | _, 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 @@ -1694,9 +1695,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else match kind_of_term x, kind_of_term y with - | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true) - | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false) - | _ -> Proofview.tclUNIT () + | Var x', _ when not (occur_term x y) -> + subst_one flags.rewrite_dependent_proof x' (hyp,y,true) + | _, Var y' when not (occur_term y x) -> + subst_one flags.rewrite_dependent_proof y' (hyp,x,false) + | _ -> + Proofview.tclUNIT () end in Proofview.Goal.nf_enter begin fun gl -> |