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

2 files changed, 36 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 ->
diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v
new file mode 100644
index 0000000000..8336f6a806
--- /dev/null
+++ b/test-suite/success/subst.v
@@ -0,0 +1,25 @@
+(* Test various subtleties of the "subst" tactics *)
+
+(* Should proceed from left to right (see #4222) *)
+Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y.
+intros.
+subst.
+change (3 = 2) in H1.
+change (3 = 3).
+Abort.
+
+(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *)
+Goal forall x y, x = y -> x = 3 -> x = y.
+intros.
+subst.
+change (3 = 3).
+Abort.
+
+(* Should substitute cycles once, until a recursive equation is obtained *)
+(* (failed in 8.4) *)
+Goal forall x y, x = S y -> y = S x -> x = y.
+intros.
+subst.
+change (y = S (S y)) in H0.
+change (S y = y).
+Abort.