Correction de la grammaire des intro-patterns

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8426 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 48 insertions, 40 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 864bd81fe..3605ebff7 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -967,11 +967,11 @@ induction n.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item{\tt induction {\term} as {\intropatterns}}
+\item{\tt induction {\term} as {\intropattern}}
 
   This behaves as {\tt induction {\term}} but uses the names in
-  {\intropatterns} to names the variables introduced in the context. The
-  list {\intropatterns} must have the form {\tt [} $p_{11}$ \ldots
+  {\intropattern} to names the variables introduced in the context. The
+  {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
   $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
   ]} with $m$ being the number of constructors of the type of
   {\term}. Each variable introduced by {\tt induction} in the context of
@@ -991,10 +991,10 @@ induction n.
 scheme of name {\qualid}. It does not expect that the type of
 {\term} is inductive.
 
-\item {\tt induction {\term} using {\qualid} as {\intropatterns}}
+\item {\tt induction {\term} using {\qualid} as {\intropattern}}
 
   This combines {\tt induction {\term} using {\qualid}}
-and {\tt induction {\term} as {\intropatterns}}.
+and {\tt induction {\term} as {\intropattern}}.
 
 \item {\tt elim \term}\label{elim}
   
@@ -1086,7 +1086,7 @@ a simple term or a term with a bindings list (see \ref{Binding-list}).
 \tacindex{destruct}
 
 The tactic {\tt destruct} is used to perform case analysis without
-recursion. Its behavior is similar to {\tt induction \term} except
+recursion. Its behavior is similar to {\tt induction} except
 that no induction hypothesis is generated.  It applies to any goal and
 the type of {\term} must be inductively defined. There are particular cases:
 
@@ -1106,11 +1106,11 @@ last introduced hypothesis.
 \end{itemize}
 
 \begin{Variants}
-\item{\tt destruct {\term} as {\intropatterns}}
+\item{\tt destruct {\term} as {\intropattern}}
 
   This behaves as {\tt destruct {\term}} but uses the names in
-  {\intropatterns} to names the variables introduced in the context. The
-  list {\intropatterns} must have the form {\tt [} $p_{11}$ \ldots
+  {\intropattern} to names the variables introduced in the context. The
+  {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
   $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
   ]} with $m$ being the number of constructors of the type of
   {\term}. Each variable introduced by {\tt destruct} in the context of
@@ -1121,17 +1121,17 @@ last introduced hypothesis.
   \ref{intros-pattern}). This provides a concise notation for nested
   destruction.
 
-  It is recommended to use this variant of {\tt destruct} for 
-  robust proof scripts.
+%  It is recommended to use this variant of {\tt destruct} for 
+%  robust proof scripts.
 
 \item{\tt destruct {\term} using {\qualid}}
 
   This is a synonym of {\tt induction {\term} using {\qualid}}.
 
-\item{\tt destruct {\term} using {\qualid} as {\intropatterns}}
+\item{\tt destruct {\term} as {\intropattern} using {\qualid}}
 
   This is a synonym of {\tt induction {\term} using {\qualid} as
-  {\intropatterns}}.
+  {\intropattern}}.
 
 \item{\tt case \term}\label{case}\tacindex{case}
   
@@ -1159,22 +1159,21 @@ last introduced hypothesis.
 
 \end{Variants}
 
-\subsection{\tt intros \intropatterns}\label{intros-pattern}
-\tacindex{intros \intropatterns}
+\subsection{\tt intros {\intropattern} {\ldots} {\intropattern}}
+\label{intros-patterns}
+\tacindex{intros \intropattern}
 
-The tactic {\tt intros} applied to a pattern performs both
+The tactic {\tt intros} applied to introduction patterns performs both
 introduction of variables and case analysis in order to give names to
 components of an hypothesis.
 
-A pattern is either:
+An introduction pattern is either:
 \begin{itemize}
 \item the wildcard: {\tt \_}
 \item a variable
-\item a list of patterns: $p_1~\ldots~p_n$
-\item a disjunction of patterns: {\tt [}$p_1$ {\tt |} {\ldots} {\tt
-|} $p_n$ {\tt ]}
-%equivalent to {\tt [}$p_1$ {\ldots} $p_n$ {\tt ]}
-%\item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )}
+\item a disjunction of lists of patterns:
+  {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
+\item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )}
 \end{itemize}
 
 The behavior of \texttt{intros} is defined inductively over the
@@ -1189,13 +1188,13 @@ introductions over the patterns namely:
 \texttt{intros $p_1$;\ldots; intros $p_n$}, the goal should start with
 at least $n$ products;
 \item introduction over a
-disjunction of patterns $[p_1~|~~\ldots~|~p_n]$, it 
-introduces a new variable $X$, its type should be an inductive
+disjunction of list of patterns
+{\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}. It introduces a new variable $X$, its type should be an inductive
 definition with $n$
 constructors, then it performs a case analysis over $X$ 
 (which generates $n$ subgoals), it 
 clears $X$ and performs on each generated subgoals the corresponding
-\texttt{intros}~$p_i$ tactic;
+\texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$ tactic;
 \item introduction over a 
 conjunction  of patterns $(p_1,\ldots,p_n)$, it
 introduces a new variable $X$, its type should be an inductive 
@@ -1205,6 +1204,12 @@ analysis over $X$
 (which generates $1$ subgoal with at least $n$ products), it 
 clears $X$ and performs an introduction over the list of patterns $p_1~\ldots~p_n$.
 \end{itemize}
+
+\Rem The pattern {\tt ($p_1$, {\ldots}, $p_n$)}
+is a synonym for the pattern {\tt [$p_1$ {\ldots} $p_n$]}, i.e. it
+corresponds to the decomposition of an hypothesis typed by an
+inductive type with a single constructor.
+
 \begin{coq_example}
 Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
 intros A B C [a| [_ c]] f.
@@ -1659,10 +1664,10 @@ introduced hypothesis.
   \tacindex{inversion\_clear}
   This behaves as \texttt{inversion} and then erases \ident~ from the
   context.
-\item \texttt{inversion} {\ident} \texttt{as} {\intropatterns} \\
+\item \texttt{inversion} {\ident} \texttt{as} {\intropattern} \\
   \tacindex{inversion \dots\ as} 
   This behaves as \texttt{inversion} but using names in
-  {\intropatterns} for naming hypotheses. The list {\intropatterns}
+  {\intropattern} for naming hypotheses. The {\intropattern}
   must have the form {\tt [} $p_{11}$ \ldots $p_{1n_1}$ {\tt |}
   {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt ]} with $m$ being
   the number of constructors of the type of {\ident}. Be careful that
@@ -1699,10 +1704,10 @@ intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ].
 Abort.
 \end{coq_eval}
 
-\item \texttt{inversion} {\num} {\tt as} {\intropatterns} \\
+\item \texttt{inversion} {\num} {\tt as} {\intropattern} \\
   This allows to name the hypotheses introduced by
   \texttt{inversion} {\num} in the context.
-\item \texttt{inversion\_clear} {\ident} {\tt as} {\intropatterns} \\
+\item \texttt{inversion\_clear} {\ident} {\tt as} {\intropattern} \\
   \tacindex{inversion\_cleardots\ as}
   This allows to name the hypotheses introduced by
   \texttt{inversion\_clear} in the context.
@@ -1711,7 +1716,7 @@ Abort.
   Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
   tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
   then performing \texttt{inversion}.
-\item \texttt{inversion } {\ident}  {\tt as} {\intropatterns}
+\item \texttt{inversion } {\ident}  {\tt as} {\intropattern}
 \texttt{in} \ident$_1$ \dots\ \ident$_n$\\
   \tacindex{inversion \dots\ as \dots\ in}
   This allows to name the hypotheses introduced in the context by
@@ -1722,7 +1727,7 @@ Abort.
   Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
   tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
   then performing {\tt inversion\_clear}.
-\item \texttt{inversion\_clear} {\ident} \texttt{as} {\intropatterns}
+\item \texttt{inversion\_clear} {\ident} \texttt{as} {\intropattern}
   \texttt{in} \ident$_1$ \ldots \ident$_n$\\ 
   \tacindex{inversion\_clear \dots\ as \dots\ in}
   This allows to name the hypotheses introduced in the context by
@@ -1732,7 +1737,7 @@ Abort.
   That must be used when \ident\ appears in the current goal. 
   It acts like \texttt{inversion} and then substitutes \ident\ for the
   corresponding term in the goal.
-\item \texttt{dependent inversion} {\ident} \texttt{as} {\intropatterns} \\
+\item \texttt{dependent inversion} {\ident} \texttt{as} {\intropattern} \\
   \tacindex{dependent inversion \dots\ as }
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion} {\ident}.
@@ -1740,7 +1745,7 @@ Abort.
   \tacindex{dependent inversion\_clear}
   Like \texttt{dependent inversion}, except that {\ident} is cleared
   from the local context.
-\item \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropatterns}\\
+\item \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropattern}\\
   \tacindex{dependent inversion\_clear \dots\ as}
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion\_clear} {\ident}
@@ -1752,7 +1757,7 @@ Abort.
   $(\vec{x}:\vec{T})s$,   then \term~  must be of type
   $I:(\vec{x}:\vec{T})(I~\vec{x})\to s'$ where $s'$ is the
   type of the goal.
-\item \texttt{dependent inversion } {\ident} \texttt{as} {\intropatterns} \texttt{ with } \term \\
+\item \texttt{dependent inversion } {\ident} \texttt{as} {\intropattern} \texttt{ with } \term \\
   \tacindex{dependent inversion \dots\ as \dots\ with}
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion } {\ident} \texttt{ with } \term.
@@ -1760,7 +1765,7 @@ Abort.
   \tacindex{dependent inversion\_clear \dots\ with}
   Like \texttt{dependent inversion \dots\ with} but clears \ident from
   the local context.
-\item \texttt{dependent inversion\_clear } {\ident} \texttt{as} {\intropatterns} \texttt{ with } \term\\
+\item \texttt{dependent inversion\_clear } {\ident} \texttt{as} {\intropattern} \texttt{ with } \term\\
   \tacindex{dependent inversion\_clear \dots\ as \dots\ with}
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term.
@@ -1769,7 +1774,7 @@ Abort.
   It is a very primitive inversion tactic that derives all the necessary
   equalities  but it does not simplify the  constraints as
   \texttt{inversion} do.
-\item \texttt{simple inversion} {\ident} \texttt{as} {\intropatterns}\\
+\item \texttt{simple inversion} {\ident} \texttt{as} {\intropattern}\\
   \tacindex{simple inversion \dots\ as}
   This allows to name the hypotheses introduced in the context by
   \texttt{simple inversion}.
@@ -1846,7 +1851,8 @@ datatype: see~\ref{quote-examples} for the full details.
   considered by \texttt{quote} as constants rather than variables.
 \end{Variants}
 
-\SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution
+% En attente d'un moyen de valoriser les fichiers de demos
+% \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution
 
 \section{Automatizing}
 \label{Automatizing}
@@ -2014,7 +2020,8 @@ incompatibilities.
   Is equivalent to {\tt intuition auto with *}.
 \end{Variants}
 
-\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
+% En attente d'un moyen de valoriser les fichiers de demos
+%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
 \subsection{{\tt firstorder}\tacindex{firstorder}}
 \label{firstorder}
@@ -2419,7 +2426,8 @@ main subgoal excluded.
 
 \SeeAlso \ref{autorewrite-example} for examples showing the use of this tactic.
 
-\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v}
+% En attente d'un moyen de valoriser les fichiers de demos
+%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v}
 
 \section{The hints databases for auto and eauto}
 \index{Hints databases}\label{Hints-databases}\comindex{Hint}
diff --git a/doc/macros.tex b/doc/macros.tex
index 9e4682c50..61ee15f5d 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -149,7 +149,7 @@
 \newcommand{\params}{\textrm{\textsl{params}}}
 \newcommand{\binderlet}{\textrm{\textsl{binder\_let}}}
 \newcommand{\pattern}{\textrm{\textsl{pattern}}}
-\newcommand{\intropatterns}{\textrm{\textsl{intro\_patterns}}}
+\newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
 \newcommand{\pat}{\textrm{\textsl{pat}}}
 \newcommand{\pgs}{\textrm{\textsl{pgms}}}
 \newcommand{\pg}{\textrm{\textsl{pgm}}}