In Regular Subst Tactic mode, ensure that the order of hypotheses is

preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.

This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.

So, I consider this to be a fix to the "Regular Subst Tactic" mode.

Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.

5 files changed, 198 insertions, 36 deletions

diff --git a/CHANGES b/CHANGES
index 79fe3642b2..6a1f8f0e49 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,6 +4,7 @@ Changes from V8.5pl1 to V8.5pl2
 Bugfixes
 
 - #4677: fix alpha-conversion in notations needing eta-expansion
+- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode.
 
 Changes from V8.5 to V8.5pl1
 ============================
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 903e2e19af..fa595d9159 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2854,42 +2854,57 @@ This tactic is deprecated. It can be replaced by {\tt enough}
 \tacindex{subst}
 \optindex{Regular Subst Tactic}
 
-This tactic applies to a goal that has \ident\ in its context and
-(at least) one hypothesis, say {\tt H}, of type {\tt
-  \ident=t} or {\tt t=\ident}. Then it replaces
-\ident\ by {\tt t} everywhere in the goal (in the hypotheses
-and in the conclusion) and clears \ident\ and {\tt H} from the context.
+This tactic applies to a goal that has \ident\ in its context and (at
+least) one hypothesis, say $H$, of type {\tt \ident} = $t$ or $t$
+{\tt = \ident} with {\ident} not occurring in $t$.  Then it replaces
+{\ident} by $t$ everywhere in the goal (in the hypotheses and in the
+conclusion) and clears {\ident} and $H$ from the context.
+
+If {\ident} is a local definition of the form {\ident} := $t$, it is
+also unfolded and cleared.
+
+\Rem
+When several hypotheses have the form {\tt \ident} = $t$ or {\tt
+  $t$ = \ident}, the first one is used.
 
 \Rem
-When several hypotheses have the form {\tt \ident=t} or {\tt
-  t=\ident}, the first one is used.
+If $H$ is itself dependent in the goal, it is replaced by the
+proof of reflexivity of equality.
 
 \begin{Variants}
-  \item {\tt subst \ident$_1$ \dots \ident$_n$}
+  \item {\tt subst \ident$_1$ {\dots} \ident$_n$}
 
-    Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
+    This is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
   \item {\tt subst}
 
-    Applies {\tt subst} repeatedly to all identifiers from the context
-    for which an equality exists.
+    This applies {\tt subst} repeatedly from top to bottom to all
+    identifiers of the context for which an equality of the form {\tt
+      \ident} = $t$ or $t$ {\tt = \ident} or {\tt \ident} := $t$ exists, with
+    {\ident} not occurring in $t$.
 
-\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set
-    Regular Subst Tactic}. When this option is activated, {\tt subst}
-  manages the following corner cases which otherwise it
-  does not:
+\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled
+using option {\tt Set Regular Subst Tactic}. When this option is
+activated, {\tt subst} also deals with the following corner cases:
 \begin{itemize}
 \item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$}
   and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a
   variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$}
-  or {\tt $u$ = \ident$_2$}
+  or {\tt $u$ = \ident$_2$}; without the option, a second call to {\tt
+    subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$
+  respectively.
+
 \item A context with cyclic dependencies as with hypotheses {\tt
-  \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$}
+  \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which
+  without the option would be a cause of failure of {\tt subst}.
 \end{itemize}
-Additionally, it prevents a local definition such as {\tt \ident :=
-  $t$} to be unfolded which otherwise it would exceptionally unfold in
+Additionally, it prevents a local definition such as {\tt \ident} :=
+  $t$ to be unfolded which otherwise it would exceptionally unfold in
 configurations containing hypotheses of the form {\tt {\ident} = $u$},
 or {\tt $u'$ = \ident} with $u'$ not a variable.
 
+Finally, it preserves the initial order of hypotheses, which without
+the option it may break.
+
 The option is off by default.
 
 \end{Variants}
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f72a72f46d..819a995db1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1595,6 +1595,17 @@ user = raise user error specific to rewrite
 (**********************************************************************)
 (* Substitutions tactics (JCF) *)
 
+let regular_subst_tactic = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "more regular behavior of tactic subst";
+      optkey   = ["Regular";"Subst";"Tactic"];
+      optread  = (fun () -> !regular_subst_tactic);
+      optwrite = (:=) regular_subst_tactic }
+
 let unfold_body x =
   Proofview.Goal.enter begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
@@ -1642,23 +1653,24 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
   let dephyps =
-    List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) ->
+    List.rev (pi3 (List.fold_right (fun (id,b,_ as dcl) (dest,deps,allhyps) ->
       if not (Id.equal id hyp)
          && List.exists (fun y -> occur_var_in_decl env y dcl) deps
       then
-        ((if b = None then deps else id::deps), id::allhyps)
+        let id_dest = if !regular_subst_tactic then dest else MoveLast in
+        (dest,(if b = None then deps else id::deps), (id_dest,id)::allhyps)
       else
-        (deps,allhyps))
+        (MoveBefore id,deps,allhyps))
       hyps
-      ([x],[]))) in
+      (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
   let depconcl = occur_var env x concl in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
-      [revert dephyps;
+      [revert (List.map snd dephyps);
        general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
-       (tclMAP intro_using dephyps)]
+       (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)]
       else
        [Proofview.tclUNIT ()]) @
      [tclTRY (clear [x; hyp])])
@@ -1709,17 +1721,6 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
-let regular_subst_tactic = ref false
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "more regular behavior of tactic subst";
-      optkey   = ["Regular";"Subst";"Tactic"];
-      optread  = (fun () -> !regular_subst_tactic);
-      optwrite = (:=) regular_subst_tactic }
-
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
   if !regular_subst_tactic then
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
new file mode 100644
index 0000000000..f5768ba441
--- /dev/null
+++ b/test-suite/output/subst.out
@@ -0,0 +1,97 @@
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+   True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+   True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+   True
+1 subgoal
+  
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+   True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+   True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+   True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+   True
+1 subgoal
+  
+  HA, HB : True
+  H4 : 0 = 4
+  H3 : 0 = 3
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+   True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
new file mode 100644
index 0000000000..e48aa6bb28
--- /dev/null
+++ b/test-suite/output/subst.v
@@ -0,0 +1,48 @@
+(* Ensure order of hypotheses is respected after "subst" *)
+
+Set Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *)
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+Unset Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+