From 8aebd0c751db55c0301518d8ed55b8ac7bccae27 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 May 2015 11:31:16 +0200
Subject: Turning "Set Regular Subst Tactic" on by default (for 8.6).

---
 doc/refman/RefMan-tac.tex  |  2 +-
 tactics/equality.ml        |  2 +-
 test-suite/success/subst.v | 25 +++++++++++++++++++++++++
 3 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/success/subst.v

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index be82eaa018..e2827d6bf7 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2841,7 +2841,7 @@ Additionally, it prevents a local definition such as {\tt \ident :=
 configurations containing hypotheses of the form {\tt {\ident} = $u$},
 or {\tt $u'$ = \ident} with $u'$ not a variable.
 
-The option is off by default.
+The option is on by default.
 
 \end{Variants}
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ea74dc37ea..d78ba8c629 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1662,7 +1662,7 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
-let regular_subst_tactic = ref false
+let regular_subst_tactic = ref true
 
 let _ =
   declare_bool_option
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.
-- 
cgit v1.2.3