From 89ec88f1e750cfb786de1929ef44fac70c9a29ab Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Sep 2016 18:45:06 +0200
Subject: Quick fix to another bug of "subst" introduced in 4e3d464 and spotted
 by Maxime.

---
 tactics/equality.ml | 5 +++--
 1 file 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 ()
-- 
cgit v1.2.3