*** empty log message ***

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

1 files changed, 107 insertions, 110 deletions

diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index b7be362578..a252a1fd98 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -72,7 +72,7 @@ is understood as
 \noindent{}\framebox[6in][l]
 {\parbox{6in}
 {\begin{center}
-\begin{tabular}{lp{0.1in}l}
+\begin{tabular}{lcl}
 {\tacexpr} & \cn{}::= &
            {\tacexpr} {\tt ;} {\tacexpr}\\
 & \cn{}| & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
@@ -135,30 +135,28 @@ is understood as
 \noindent{}\framebox[6in][l]
 {\parbox{6in}
 {\begin{center}
-\begin{tabular}{lp{0.1in}l}
-\tacarg & \cn{}::= & 
-           {\qualid}\\
-& \cn{}| & {\tt ()} \\
-& \cn{}| & {\tt ltac :} {\atom}\\
-& \cn{}| & {\term}\\
+\begin{tabular}{lcl}
+\tacarg & ::= & 
+        {\qualid}\\
+& $|$ & {\tt ()} \\
+& $|$ & {\tt ltac :} {\atom}\\
+& $|$ & {\term}\\
 \\
-\letclause & \cn{}::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
+\letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
 \\
-\recclause & \cn{}::= & {\ident} \nelist{\name}{} {\tt :=} {\tacexpr}\\
+\recclause & ::= & {\ident} \nelist{\name}{} {\tt :=} {\tacexpr}\\
 \\
-\contextrule & \cn{}::= &
-  \nelist{\contexthyps}{\tt ,} {\tt |-}
-{\cpattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt \_ =>} {\tacexpr}\\
+\contextrule & ::= &
+  \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
+& $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
+& $|$ & {\tt \_ =>} {\tacexpr}\\
 \\
-\contexthyps & \cn{}::= &
-           {\name} {\tt :} {\cpattern}\\
+\contexthyps & ::= & {\name} {\tt :} {\cpattern}\\
 \\
-\matchrule & \cn{}::= &
+\matchrule & ::= &
            {\cpattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt \_ =>} {\tacexpr}\\
+& $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
+& $|$ & {\tt \_ =>} {\tacexpr}\\
 \end{tabular}
 \end{center}}}
 \caption{Syntax of the tactic language (continued)}
@@ -169,10 +167,10 @@ is understood as
 \noindent{}\framebox[6in][l]
 {\parbox{6in}
 {\begin{center}
-\begin{tabular}{lp{0.1in}l}
-\nterm{top} & \cn{}::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
+\begin{tabular}{lcl}
+\nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
-\nterm{ltac\_def} & \cn{}::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
+\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
 \end{tabular}
 \end{center}}}
 \caption{Tactic toplevel definitions}
@@ -247,10 +245,10 @@ of Ltac.
 \index{;@{\tt ;}}
 \index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
 
-A sequence is an expression of the following form:\\
-
-{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$\\
-
+A sequence is an expression of the following form:
+\begin{center}
+{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
+\end{center}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied
 and $v_2$ is applied to every subgoal generated by the application of
@@ -261,11 +259,11 @@ $v_1$. Sequence is left associating.
 \index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
 \index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
-We can generalize the previous sequence operator by:\\
-
+We can generalize the previous sequence operator by:
+\begin{center}
 {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
-{\tacexpr}$_n$ {\tt ]}\\
-
+{\tacexpr}$_n$ {\tt ]}
+\end{center}
 {\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is
 applied and $v_i$ is applied to the $i$-th generated subgoal by the
 application of $v_0$, for $=1,...,n$. It fails if the application of
@@ -275,10 +273,10 @@ $v_0$ does not generate exactly $n$ subgoals.
 \tacindex{do}
 \index{Tacticals!do@{\tt do}}
 
-There is a for loop that repeats a tactic {\num} times:\\
-
-{\tt do} {\num} {\tacexpr}\\
-
+There is a for loop that repeats a tactic {\num} times:
+\begin{center}
+{\tt do} {\num} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied {\num} times. Supposing ${\num}>1$, after the first
 application of $v$, $v$ is applied, at least once, to the generated
@@ -289,10 +287,10 @@ the {\num} applications have been completed.
 \tacindex{repeat}
 \index{Tacticals!repeat@{\tt repeat}}
 
-We have a repeat loop with:\\
-
-{\tt repeat} {\tacexpr}\\
-
+We have a repeat loop with:
+\begin{center}
+{\tt repeat} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied until it fails. Supposing $n>1$, after the first application
 of $v$, $v$ is applied, at least once, to the generated subgoals and
@@ -303,10 +301,10 @@ fails.
 \tacindex{try}
 \index{Tacticals!try@{\tt try}}
 
-We can catch the tactic errors with:\\
-
-{\tt try} {\tacexpr}\\
-
+We can catch the tactic errors with:
+\begin{center}
+{\tt try} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ fails, it catches the error and
 leaves the goal unchanged. If the level of the exception is positive,
@@ -315,10 +313,10 @@ then the exception is re-raised with its level decremented.
 \subsubsection{Detecting progress}
 \tacindex{progress}
 
-We can check if a tactic made progress with:\\
-
-{\tt progress} {\tacexpr}\\
-
+We can check if a tactic made progress with:
+\begin{center}
+{\tt progress} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ produced one subgoal equal to the
 initial goal (up to syntactical equality), then an error of level 0 is
@@ -331,10 +329,10 @@ raised.
 \tacindex{||}
 \index{Tacticals!orelse@{\tt ||}}
 
-We can easily branch with the following structure:\\
-
-{\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$\\
-
+We can easily branch with the following structure:
+\begin{center}
+{\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
+\end{center}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if
 it fails then $v_2$ is applied. Branching is left associating.
@@ -344,13 +342,13 @@ it fails then $v_2$ is applied. Branching is left associating.
 \index{Tacticals!first@{\tt first}}
 
 We may consider the first tactic to work (i.e. which does not fail) among a
-panel of tactics:\\
-
-{\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\
-
+panel of tactics:
+\begin{center}
+{\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+\end{center}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it
-tries to apply $v_2$ and so on. It fails when there is no applicable tactic.\\
+tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
 
 \ErrMsg \errindex{No applicable tactic}
 
@@ -359,13 +357,13 @@ tries to apply $v_2$ and so on. It fails when there is no applicable tactic.\\
 \index{Tacticals!solve@{\tt solve}}
 
 We may consider the first to solve (i.e. which generates no subgoal) among a
-panel of tactics:\\
-
-{\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\
-
+panel of tactics:
+\begin{center}
+{\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+\end{center}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it
-tries to apply $v_2$ and so on. It fails if there is no solving tactic.\\
+tries to apply $v_2$ and so on. It fails if there is no solving tactic.
 
 \ErrMsg \errindex{Cannot solve the goal}
 
@@ -374,10 +372,10 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.\\
 \index{Tacticals!idtac@{\tt idtac}}
 
 The constant {\tt idtac} is the identity tactic: it leaves any goal
-unchanged but it appears in the proof script.\\
-
-{\tt idtac} and {\tt idtac "message"}\\
-
+unchanged but it appears in the proof script.
+\begin{center}
+{\tt idtac} and {\tt idtac "message"}
+\end{center}
 The latter variant prints the string on the standard output.
 
 \subsubsection{Failing}
@@ -386,10 +384,10 @@ The latter variant prints the string on the standard output.
 
 The tactic {\tt fail} is the always-failing tactic: it does not solve
 any goal. It is useful for defining other tacticals since it can be
-catched by {\tt try} or {\tt match goal}. There are three variants:\\
-
-{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}  \\
-
+catched by {\tt try} or {\tt match goal}. There are three variants:
+\begin{center}
+{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}
+\end{center}
 The number $n$ is the failure level. If no level is specified, it
 defaults to $0$.  The level is used by {\tt try} and {\tt match goal}.
 If $0$, it makes {\tt match goal} considering the next clause
@@ -428,10 +426,10 @@ argument is required.
 
 \subsubsection{Application}
 
-An application is an expression of the following form:\\
-
-{\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$\\
-
+An application is an expression of the following form:
+\begin{center}
+{\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$
+\end{center}
 The reference {\qualid} must be bound to some defined tactic
 definition expecting at least $n$ arguments.  The expressions
 {\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$.
@@ -446,10 +444,10 @@ definition expecting at least $n$ arguments.  The expressions
 \tacindex{fun}
 
 A parameterized tactic can be built anonymously (without resorting to
-local definitions) with:\\
-
-{\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}\\
-
+local definitions) with:
+\begin{center}
+{\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}
+\end{center}
 Indeed, local definitions of functions are a syntactic sugar for
 binding a {\tt fun} tactic to an identifier.
 
@@ -477,21 +475,21 @@ pattern {\_} matches any term and shunts all remaining patterns if
 any. If {\tacexpr}$_1$ evaluates to a tactic, this tactic is not
 immediately applied to the current goal (in contrast with {\tt match
 goal}). If all clauses fail (in particular, there is no pattern {\_})
-then a no-matching error is raised. \\
+then a no-matching error is raised.
 
 \begin{ErrMsgs}
 \item \errindex{No matching clauses for match}\\
-\hx{4}No pattern can be used and, in particular, there is no {\tt \_} pattern.
+No pattern can be used and, in particular, there is no {\tt \_} pattern.
 \item \errindex{Argument of match does not evaluate to a term}\\
-\hx{4}This happens when {\tacexpr} does not denote a term.
+This happens when {\tacexpr} does not denote a term.
 \end{ErrMsgs}
 
 \tacindex{context (in pattern)}
 There is a special form of patterns to match a subterm against the
-pattern:\\
-
-{\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}\\
-
+pattern:
+\begin{center}
+{\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
+\end{center}
 It matches any term which one subterm matches {\cpattern}. If there is
 a match, the optional {\ident} is assign the ``matched context'', that
 is the initial term where the matched subterm is replaced by a
@@ -537,11 +535,13 @@ hypotheses is tried with the same proof context pattern. If there is
 no other combination of hypotheses then the second proof context
 pattern is tried and so on. If the next to last proof context pattern
 fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$
-is applied.\\
+is applied.
+
+\ErrMsg \errindex{No matching clauses for match goal}
 
-\ErrMsg \errindex{No matching clauses for match goal}\\
-\hx{4}No goal pattern can be used and, in particular, there is no {\tt
+No goal pattern can be used and, in particular, there is no {\tt
 \_} goal pattern.
+\medskip
 
 It is important to know that each hypothesis of the goal can be
 matched by at most one hypothesis pattern. The order of matching is
@@ -557,9 +557,9 @@ the {\tt match reverse goal with} variant.
 The following expression is not a tactic in the sense that it does not
 produce subgoals but generates a term to be used in tactic
 expressions:
-
+\begin{center}
 {\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]}
-
+\end{center}
 {\ident} must denote a context variable bound by a {\tt context}
 pattern of a {\tt match} expression. This expression evaluates
 replaces the hole of the value of {\ident} by the value of
@@ -575,18 +575,16 @@ the system decide a name with the {\tt intro} tactic is not so good
 since it is very awkward to retrieve the name the system gave.
 
 As before, the following expression returns a term:
-
+\begin{center}
 {\tt fresh} {\qstring}
-
+\end{center}
 It evaluates to an identifier unbound in the goal, which is obtained
 by padding {\qstring} with a number if necessary. If no name is given,
 the prefix is {\tt H}.
 
-\subsubsection{Type of a constr}
+\subsubsection{{\tt type of} {\term}}
 \tacindex{type of}
 
-{\tt type of} {\term}
-
 This tactic computes the type of {\term}.
 
 
@@ -594,9 +592,9 @@ This tactic computes the type of {\term}.
 \tacindex{eval}
 
 Evaluation of a term can be performed with:
-
-{\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
-
+\begin{center}
+{\tt eval} {\nterm{redexpr}} {\tt in} {\term}
+\end{center}
 where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt
 hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
 {\tt fold}, {\tt pattern}.
@@ -635,30 +633,28 @@ without having to cut manually the proof in smaller lemmas.
 \subsection{Tactic toplevel definitions}
 \comindex{Ltac}
 
-Basically, tactics toplevel definitions are made as follows:\\
-
+Basically, tactics toplevel definitions are made as follows:
 %{\tt Tactic Definition} {\ident} {\tt :=} {\tacexpr}\\
 %
 %{\tacexpr} is evaluated to $v$ and $v$ is associated to {\ident}. Next, every
 %script is evaluated by substituting $v$ to {\ident}.
 %
 %We can define functional definitions by:\\
-
+\begin{center}
 {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
-{\tacexpr}\\
-
-\noindent This defines a new tactic that can be used in any tactic
-script or new tactic toplevel definition.
-
-\Rem The preceding definition can equivalently be written:\\
+{\tacexpr}
+\end{center}
+This defines a new tactic that can be used in any tactic script or new
+tactic toplevel definition.
 
+\Rem The preceding definition can equivalently be written:
+\begin{center}
 {\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$
-{\tt =>} {\tacexpr}\\
-
-\noindent Recursive and mutual recursive function definitions are also
+{\tt =>} {\tacexpr}
+\end{center}
+Recursive and mutual recursive function definitions are also
 possible with the syntax:
-\medskip
-
+\begin{center}
 \begin{tabular}{l}
 {\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ...
 {\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\
@@ -668,6 +664,7 @@ possible with the syntax:
 {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
 {\tacexpr}$_n$
 \end{tabular}
+\end{center}
 
 %This definition bloc is a set of definitions (use of
 %the same previous syntactical sugar) and the other scripts are evaluated as