Merge branch 'v8.5'

1 files changed, 7 insertions, 7 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ddb48b0c1b..18bcd1af62 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -813,7 +813,7 @@ either:
   \item the pattern \texttt{?\ident}
   \item an identifier
   \end{itemize}
-\item a {\em destructing introduction pattern} which itself classifies into:
+\item an {\em action introduction pattern} which itself classifies into:
   \begin{itemize}
   \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
     \begin{itemize}
@@ -828,9 +828,9 @@ either:
     \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
     \item the rewriting orientations: {\tt ->} or {\tt <-}
     \end{itemize}
-  \item the on-the-fly application of lemmas: $p${\tt /{\term$_1$}}
-    \ldots {\tt /{\term$_n$}} where $p$ itself is not an on-the-fly
-    application of lemmas pattern
+  \item the on-the-fly application of lemmas: $p${\tt \%{\term$_1$}}
+    \ldots {\tt \%{\term$_n$}} where $p$ itself is not a pattern for
+    on-the-fly application of lemmas (note: syntax is in experimental stage)
   \end{itemize}
 \item the wildcard: {\tt \_}
 \end{itemize}
@@ -898,10 +898,10 @@ introduction pattern~$p$:
   itself is erased; if the term to substitute is a variable, it is
   substituted also in the context of goal and the variable is removed
   too;
-\item introduction over a pattern $p${\tt /{\term$_1$}} \ldots {\tt
-  /{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the
+\item introduction over a pattern $p${\tt \%{\term$_1$}} \ldots {\tt
+  \%{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the
   hypothesis to be introduced (as in {\tt apply }{\term}$_1$, \ldots,
-  {\term}$_n$ {\tt in}), prior to the application of the introduction
+  {\term}$_n$ {\tt in}) prior to the application of the introduction
   pattern $p$;
 \item introduction on the wildcard depends on whether the product is
   dependent or not: in the non-dependent case, it erases the