diff options
| author | Pierre-Marie Pédrot | 2016-10-02 15:24:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-02 15:24:24 +0200 |
| commit | decdd5b3cc322936f7d1e7cc3bb363a2957d404e (patch) | |
| tree | e3249cf6ea5950653c4b985c872959277a383a88 | |
| parent | 466b7e69e49a5f4bba36b834a2e046f120ece07c (diff) | |
| parent | 89ec88f1e750cfb786de1929ef44fac70c9a29ab (diff) | |
Merge branch 'v8.5' into v8.6
| -rw-r--r-- | tactics/equality.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 26e4f01f2b..201a1e00e8 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1783,15 +1783,16 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let process hyp = Proofview.Goal.enter { enter = begin fun 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 c = pf_get_hyp hyp gl |> get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* 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', _ when not (occur_term x y) -> + | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (occur_term y x) -> + | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () |