Mise en place avertissements pour rep�rer les erreurs volontaires de coq-tex

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

10 files changed, 121 insertions, 28 deletions

diff --git a/doc/Cases.tex b/doc/Cases.tex
index f9840bf5b..5b218e83e 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -190,6 +190,12 @@ the second one.
 
 Terms with useless patterns are not accepted by the
 system. Here is an example:
+% Test failure
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(**************** Error: This clause is redundant ********************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Check [x:nat]Cases x of O => true | (S _) => false | x => true end.
 \end{coq_example}
@@ -218,6 +224,12 @@ Check [l:(List nat)]Cases l of
 
 
 When we use parameters in patterns there is an error message:
+% Test failure
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(******** Error: The constructor cons expects 2 arguments ************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Check [l:(List nat)]Cases l of 
                              (nil A)      => (nil nat)
@@ -385,8 +397,14 @@ type of $e_1\ldots e_n$).
 When the arity of the predicate (i.e. number of abstractions) is not
 correct Coq raises an error message. For example:
 
+% Test failure
 \begin{coq_eval}
 Reset concat.
+(********** The following is not correct and should produce **********)
+(**** Error: The elimination predicate [n:nat](listn (plus n m))  ****)
+(*** should be of arity nat->nat->Type (for non dependent case) or ***)
+(** (n:nat)(listn n)->(n0:nat)(listn n0)->Type (for dependent case) **)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
 \end{coq_eval}
 
 \begin{coq_example}
diff --git a/doc/Program.tex b/doc/Program.tex
index 9fd6080b8..ddcf8d920 100644
--- a/doc/Program.tex
+++ b/doc/Program.tex
@@ -415,7 +415,7 @@ Suppose we give the following definitions in \Coq:
 
 First, the decidability of the ordering relation:
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 Require Le.
 Require Gt.
 \end{coq_eval}
@@ -531,7 +531,7 @@ Suppose we give the following definitions in \Coq:
 
 Declaration of the ordering relation:
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 Require List.
 Require Gt.
 \end{coq_eval}
@@ -542,7 +542,7 @@ Hypothesis inf_sup : (x,y:A){(inf x y)}+{(sup x y)}.
 \end{coq_example*}
 Definition of the concatenation of two lists:
 \begin{coq_eval}
-Save State toto.
+Write State toto.
 \end{coq_eval}
 \begin{coq_example*}
 Fixpoint app [l:list] : list -> list 
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 81f2c04a7..483fedbb8 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -624,6 +624,11 @@ parameters are applied in the correct manner in each recursive call.
 In particular, the following definition will not be accepted because 
 there is an occurrence of \List\ which is not applied to the parameter
 variable:
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(********* Error: The 1st argument of list' must be A in ... *********)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Inductive list' [A : Set] : Set := 
      nil' : (list' A) | cons' : A -> (list' A->A) -> (list' A).
@@ -1191,7 +1196,7 @@ But assuming the definition of a son function from \tree\ to \forest:
 The following is not a conversion but can be proved after a case analysis.
 \begin{coq_example}
 Goal (t:tree)(sizet t)=(S (sizef (sont t))).
-(* this one fails *)
+(** this one fails **)
 Reflexivity.
 Destruct t.
 Reflexivity.
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 75e45de46..5fc9aac26 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -63,7 +63,7 @@ manifest) fields. For instance, {\tt Record} {\ident} {\tt [}
 \Example
 The set of rational numbers may be defined as:
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
 Record Rat : Set := mkRat {
@@ -142,7 +142,7 @@ Eval Compute in (bottom half).
 Eval Compute in (Rat_bottom_cond half).
 \end{coq_example}
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 \end{coq_eval}
 
 \begin{Warnings}
@@ -901,11 +901,21 @@ Print the list of valid path coercions in the current context.
 \comindex{Set Printing Coercions}
 \comindex{Unset Printing Coercions}
 
-This command forces the coercions to be printed.
+This command forces all the coercions to be printed.
 To skip the printing of coercions, use
  {\tt Unset Printing Coercions.}.
 By default, coercions are not printed.
 
+\subsubsection{\tt Set Printing Coercion {\qualid}.}
+\comindex{Set Printing Coercions}
+\comindex{Unset Printing Coercions}
+
+This command forces coercion denoted by {\qualid} to be printed.
+To skip the printing of coercion {\qualid}, use
+ {\tt Unset Printing Coercion {\qualid}.}.
+By default, a coercion is never printed.
+
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 2550bc488..e74d286d2 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -934,9 +934,6 @@ Inductive
 with forest [A,B:Set] : Set := leaf : B -> (forest A B)
                    | cons : (tree A B) -> (forest A B) -> (forest A B).
 \end{coq_example*}
-\begin{coq_eval}
-Save State toto.
-\end{coq_eval}
 
 Assume we define an inductive definition inside a section.  When the
 section is closed, the variables declared in the section and occurring
@@ -1049,6 +1046,11 @@ decreases because it is a {\em pattern variable} coming from {\tt Cases
 \Example The following definition is not correct and generates an
 error message:
 
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(********* Error: Recursive call applied to an illegal term **********)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Fixpoint wrongplus [n:nat] : nat->nat 
    := [m:nat]Cases m of O => n | (S p) => (S (wrongplus n p)) end.
@@ -1092,7 +1094,7 @@ generally any mutually recursive definitions.
 \Example 
 The size of trees and forests can be defined the following way: 
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 Variables A,B:Set.
 Inductive tree : Set :=  node : A -> forest -> tree
 with forest : Set := leaf : B -> forest 
@@ -1137,6 +1139,11 @@ the single recursive call of \texttt{from} is guarded by an
 application of \texttt{Seq}. On the contrary, the following recursive
 function does not satisfy the guard condition:
 
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(***************** Error: Unguarded recursive call *******************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example*}
 CoFixpoint filter  : (nat->bool)->Stream->Stream := 
    [p:nat->bool]
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 69d1257f6..df4e12c38 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -101,6 +101,14 @@ First, we find propositional calculus connectives:
 \ttindex{proj1}
 \ttindex{proj2}
 
+\begin{coq_eval}
+(* We restate the grammar rule for /\ and \/ since *)
+(* it is only valid to parce Coq.Init.Logic.and *)
+Grammar constr constr6 :=
+  myand [ constr5($c1) "/\\" constr6($c2) ] -> [ (and $c1 $c2) ]
+with constr7 :=
+  myor [ constr6($c1) "\\/" constr7($c2) ] -> [ (or $c1 $c2) ].
+\end{coq_eval}
 \begin{coq_example*}
 Inductive True : Prop := I : True. 
 Inductive False : Prop := . 
@@ -272,11 +280,16 @@ again defined as inductive constructions over the sort
 \ttindex{nat}
 \ttindex{O}
 \ttindex{S}
+\ttindex{option}
+\ttindex{Some}
+\ttindex{None}
 
 \begin{coq_example*}
 Inductive unit : Set := tt : unit.
 Inductive bool : Set := true : bool 
                       | false : bool.
+Inductive option [A:Set] : Set := Some : A -> (option A)
+                                | None : (option A).
 Inductive nat : Set := O : nat 
                      | S : nat->nat.
 \end{coq_example*}
@@ -452,7 +465,7 @@ Abort.
 Abort.
 \end{coq_eval}
 
-The next construct builds a sum between a data type \verb|A:Set| and
+The next constructs builds a sum between a data type \verb|A:Set| and
 an exceptional value encoding errors:
 
 \ttindex{Exc}
@@ -460,8 +473,9 @@ an exceptional value encoding errors:
 \ttindex{error}
 
 \begin{coq_example*}
-Inductive Exc [A:Set] : Set := value : A->(Exc A) 
-                             | error : (Exc A).
+Definition Exc := option.
+Definition value := Some.
+Definition error := None.
 \end{coq_example*}
 
 
@@ -888,7 +902,7 @@ Reset Initial.
 
 \begin{coq_example*}
 Require Arith.
-Fixpoint even [n:nat] : nat :=
+Fixpoint even [n:nat] : bool :=
 Cases n of (0) => true 
         |  (1) => false
         | (S (S n)) => (even n)
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index a83a2a74e..e127a0d79 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -503,6 +503,11 @@ This command gives the status of the \Coq\ module {\dirpath}. If the module is l
 This command displays the full name of the qualified identifier {\qualid}
 and consequently the \Coq\ module in which it is defined.
 
+\begin{coq_eval}
+(***************** The last line should produce **************************)
+(************* Error: I.Dont.Exist not a defined object ******************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Locate nat.
 Locate Datatypes.O.
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 1632faedf..87a0ea799 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -539,7 +539,7 @@ rule with identifiers and not metavariables, an error occurs:
 % Test failure
 \begin{coq_example}
 Grammar constr constr1 := 
-  not_eq [ command0(a) "#" command0(b) ] -> [~(a=b)].
+  not_eq [ constr0($a) "#" constr0($b) ] -> [~(a=b)].
 \end{coq_example}
 
 For instance, let us give the statement of the symmetry of \verb+#+:
@@ -566,7 +566,7 @@ effect as ``{\tt Goal term.}''.
 
 \begin{coq_example}
 Grammar vernac vernac := 
-  thesis [ "|" "-" constr:constr($term) "." ]
+  thesis [ "|-" constr:constr($term) "." ]
           -> [Goal $term.].
 \end{coq_example}
 
@@ -574,7 +574,7 @@ Grammar vernac vernac :=
 dash, as in
 
 \begin{coq_example}
-| - (A:Prop)A->A.
+|- (A:Prop)A->A.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -587,7 +587,7 @@ token:
 
 \begin{coq_example}
 Grammar vernac vernac := 
-  thesis [ "|-" command:command($term) "." ]
+  thesis [ "|-" constr:constr($term) "." ]
           -> [Goal $term.].
 | - (A:Prop)A->A.
 \end{coq_example}
@@ -775,6 +775,11 @@ parsed with the term parser.
 \noindent The problem is that sometimes, the intermediate {\tt SQUASH}
 node cannot re-shaped, then we have a very specific error:
 
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(************** Error: Ill-formed specification **********************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Check {True}.
 \end{coq_example}
@@ -800,6 +805,11 @@ Check ([x:nat]x || [y:nat]y).
 pattern matching succeeds. It fails when the two terms are not equal:
 
 % Test failure
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(************* Error: ...  Grammar case failure ... ******************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Check ([x:nat]x || [z:bool]z).
 \end{coq_example}
@@ -848,6 +858,11 @@ depends on the universe name. The following command fails because {\tt
 ne\_identarg\_list} is already defined with type {\tt ast list} but the
 {\tt Grammar} command header assumes its type is {\tt ast}.
 
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(****** Error: ne_identarg_list already exists with another type *****)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 % Test failure
 \begin{coq_example}           
 Grammar tactic ne_identarg_list :=
@@ -860,6 +875,11 @@ has been already defined with type {\tt Ast}, and cannot be extended
 with a rule returning AST lists.
 
 % Test failure
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(********* Error: ']' expected after [default_action_parser] *********)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}           
 Grammar constr constr1 :=
   carret_list [ constr0($c1) "^" constr0($c2)] -> [ $c1 $c2 ].
@@ -908,6 +928,11 @@ avoid these troubles. The problem arises in the {\gallina} syntax, to
 make {\camlpppp} factorize the rules for application and product. The
 natural grammar would be:
 
+% Test failure
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(******** Syntax error: ')' expected after [Constr.constr10] *********)
+\end{coq_eval}
 \begin{coq_example}
 Grammar constr constr0 : ast :=
   parenthesis [ "(" constr10($c) ")" ] -> [$c]
@@ -919,7 +944,6 @@ with constr10 : ast :=
 | inject_com91 [ constr9($c) ] -> [$c].
 Check (x:nat)nat.
 \end{coq_example}
-% Test failure
 
 \begin{coq_eval}
 Reset Initial.
@@ -943,6 +967,11 @@ the right-hand side of the rule, but the error message in the
 following example would not be as relevant:
 
 % Test failure
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(******* Error: This expression should be a simple identifier ********)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Check (S O:nat)nat.
 \end{coq_example}
@@ -1054,7 +1083,7 @@ order for a user-defined tactic:
 \begin{coq_example*}
 Declare ML Module "eqdecide".
 Syntax tactic level 0:
-  ComparePP [(Compare $com1 $com2)]    -> 
+  Compare_PP [(Compare $com1 $com2)]    -> 
             ["Compare" [1 2] $com1 [1 2] $com2].
 \end{coq_example*}
 
@@ -1142,7 +1171,7 @@ but preceded by \verb+$+.
 \end{itemize}
 
 Note that while grammar rules are related by the name of non-terminals
-(such as {\tt command6} and {\tt command7}) printing rules are
+(such as {\tt constr6} and {\tt constr7}) printing rules are
 isolated. The {\tt Pxor} rule tells how to print an {\tt Xor}
 expression but not how to print its subterms.  The printer looks up
 recursively the rules for the values of \verb+$t1+ and \verb+$t2+. The
@@ -1700,7 +1729,7 @@ understand what is happening. The printers are in the file {\tt
 src/typing/printer}. There you will find the functions:
 
 \begin{itemize}
-\item {\tt gencompr} : the printer of commands
+\item {\tt prterm} : the printer of constructions
 \item {\tt gentacpr} : the printer of tactics
 \end{itemize}
 
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 49dd8a437..b7f9680b3 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -121,6 +121,11 @@ Goal (R n p).
 The direct application of {\tt Rtrans} with {\tt Apply} fails because
 no value for {\tt y} in {\tt Rtrans} is found by {\tt Apply}:
 
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Apply Rtrans.
 \end{coq_example}
@@ -192,7 +197,7 @@ The definition of principle of mutual induction for {\tt tree} and
 {\tt forest} over the sort {\tt Set} is defined by the command:
 
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 Variables A,B:Set.
 Mutual Inductive tree : Set :=  node : A -> forest -> tree
 with forest : Set := leaf : B -> forest 
@@ -226,7 +231,7 @@ Check forest_tree_rec.
 Let {\tt odd} and {\tt even} be inductively defined as:
 
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 \end{coq_eval}
 
 \begin{coq_example*}
@@ -299,7 +304,7 @@ Let's consider the relation \texttt{Le} over natural numbers and the
 following variables:
 
 \begin{coq_eval}
-Restore State Initial.
+Reset Initial.
 \end{coq_eval}
 
 \begin{coq_example*}
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index dd5b0ff5f..b192e0d0e 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -32,7 +32,7 @@ he does not use any special interface such as Emacs or Centaur.
 Instructions on installation procedures, as well as more comprehensive
 documentation, may be found in the standard distribution of \Coq,
 which may be obtained by anonymous FTP from site \verb:ftp.inria.fr:,
-directory \verb:INRIA/coq/V7.0:. 
+directory \verb:INRIA/coq/V7.1:. 
 
 In the following, all examples preceded by the prompting sequence
 \verb:Coq < : represent user input, terminated by a period. The
@@ -46,7 +46,7 @@ The standard invocation of \Coq\ delivers a message such as:
 \begin{flushleft}
 \begin{verbatim}
 unix:~> coqtop
-Welcome to Coq 7.0 (April 2001)
+Welcome to Coq 7.1 (September 2001)
 
 Coq < 
 \end{verbatim}