From 27689bac62f85c039517cbd003f8ea74cb9b4aa7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 24 Apr 2016 18:22:53 +0200
Subject: 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.
---
 doc/refman/RefMan-tac.tex | 53 ++++++++++++++++++++++++++++++-----------------
 1 file changed, 34 insertions(+), 19 deletions(-)

(limited to 'doc')

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}
-- 
cgit v1.2.3