diff options
| author | Hugo Herbelin | 2016-09-30 18:45:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-30 19:20:40 +0200 |
| commit | 89ec88f1e750cfb786de1929ef44fac70c9a29ab (patch) | |
| tree | 9b8521eff78cd358bbdb6bb1b8dfa2df22ac2dd0 | |
| parent | c78af970e1f003587fba9bebdf3ab5ca3b23face (diff) | |
Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.
| -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 b4c027382a..95b3e2b779 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1752,15 +1752,16 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let process hyp = Proofview.Goal.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 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 () |