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.

1 files changed, 34 insertions, 19 deletions

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}