Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.

Author: herbelin

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 ()