Fixing treatment of recursive equations damaged by 857e82b2ca0d1.

Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).

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