Preprend Fail to all the expected failures in the documentation.

This commit also removes comments from Coq examples, as they cause
extraneous delayed prompts that clutter the output because coq_tex cannot
remove them. Some documentation errors were also fixed in the process,
since they are easier to spot now that only unexpected failures stand out.

8 files changed, 49 insertions, 63 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 51ec2ef81..4238bf6a5 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -194,7 +194,7 @@ system. Here is an example:
 Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
-Check (fun x:nat =>
+Fail Check (fun x:nat =>
          match x with
          | O => true
          | S _ => false
@@ -271,7 +271,7 @@ When we use parameters in patterns there is an error message:
 Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
-Check
+Fail Check
   (fun l:List nat =>
      match l with
      | nil A => nil nat
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 069b99127..e8ebb9f99 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -107,7 +107,7 @@ satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be
 found, an error is raised:
 
 \begin{coq_example}
-Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
+Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 The algorithm used to solve constraints is a variant of the eauto tactic
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 1cce48b95..3fd5ae0b2 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -742,11 +742,11 @@ there is an occurrence of \List\ which is not applied to the parameter
 variable in the conclusion of the type of {\tt cons'}:
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(********* Error: The 1st argument of list' must be A in ... *********)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (********* Error: The 1st argument of list' must be A in ... *********)
 \begin{coq_example}
-Inductive list' (A:Set) : Set :=
+Fail Inductive list' (A:Set) : Set :=
   | nil' : list' A
   | cons' : A -> list' A -> list' (A*A).
 \end{coq_example}
@@ -919,12 +919,10 @@ Inductive exProp (P:Prop->Prop) : Prop
   := exP_intro : forall X:Prop, P X -> exProp P.
 \end{coq_example*}
 The same definition on \Set{} is not allowed and fails:
-\begin{coq_eval}
-(********** The following is not correct and should produce **********)
-(*** Error: Large non-propositional inductive types must be in Type***)
-\end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (*** Error: Large non-propositional inductive types must be in Type***)
 \begin{coq_example}
-Inductive exSet (P:Set->Prop) : Set 
+Fail Inductive exSet (P:Set->Prop) : Set
   := exS_intro : forall X:Set, P X -> exSet P.
 \end{coq_example}
 It is possible to declare the same inductive definition in the
@@ -1282,14 +1280,11 @@ Inductive or (A B:Prop) : Prop :=
 \end{coq_example*}
 The following definition which computes a boolean value by case over
 the proof of \texttt{or A B} is not accepted:
-\begin{coq_eval}
-(***************************************************************)
-(*** This example should fail with ``Incorrect elimination'' ***)
-\end{coq_eval}
+% (***************************************************************)
+% (*** This example should fail with ``Incorrect elimination'' ***)
 \begin{coq_example}
-Set Asymmetric Patterns.
-Definition choice (A B: Prop) (x:or A B) := 
-   match x with or_introl a => true | or_intror b => false end.
+Fail Definition choice (A B: Prop) (x:or A B) :=
+  match x with or_introl _ _ a => true | or_intror _ _ b => false end.
 \end{coq_example}
 From the computational point of view, the structure of the proof of
 \texttt{(or A B)} in this term is needed for computing the boolean
@@ -1592,8 +1587,8 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
 Print plus.
 Fixpoint lgth (A:Set) (l:list A) {struct l} : nat :=
   match l with
-  | nil => O
-  | cons a l' => S (lgth A l')
+  | nil _ => O
+  | cons _ a l' => S (lgth A l')
   end.
 Print lgth.
 Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f)
@@ -1632,13 +1627,11 @@ Definition sont (t:tree) : forest
    := let (f) := t in f.
 \end{coq_example}
 The following is not a conversion but can be proved after a case analysis.
-\begin{coq_eval}
-(******************************************************************)
-(** Error: Impossible to unify ....                              **)
-\end{coq_eval}
+% (******************************************************************)
+% (** Error: Impossible to unify ....                              **)
 \begin{coq_example}
 Goal forall t:tree, sizet t = S (sizef (sont t)).
-reflexivity. (** this one fails **)
+Fail reflexivity.
 destruct t.
 reflexivity.
 \end{coq_example}
@@ -1701,16 +1694,13 @@ by using the compiler option \texttt{-impredicative-set}.
 
 For example, using the ordinary \texttt{coqtop} command, the following
 is rejected.
-\begin{coq_eval}
-(** This example should fail *******************************
-    Error: The term forall X:Set, X -> X has type Type
-    while it is expected to have type Set
-***)
-\end{coq_eval}
+% (** This example should fail *******************************
+%     Error: The term forall X:Set, X -> X has type Type
+%     while it is expected to have type Set ***)
 \begin{coq_example}
-Definition id: Set := forall X:Set,X->X.
+Fail Definition id: Set := forall X:Set,X->X.
 \end{coq_example}
-while it will type-check, if one use instead the \texttt{coqtop
+while it will type-check, if one uses instead the \texttt{coqtop
   -impredicative-set} command.
 
 The major change in the theory concerns the rule for product formation
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex
index c84e3a9df..aae10e323 100644
--- a/doc/refman/RefMan-decl.tex
+++ b/doc/refman/RefMan-decl.tex
@@ -192,7 +192,7 @@ later.
 Theorem this_is_not_so_trivial: False.
 proof.
 end proof. (* here a warning is issued *)
-Qed. (* fails: the proof in incomplete *)
+Fail Qed. (* fails: the proof in incomplete *)
 Admitted. (* Oops! *)
 \end{coq_example}
 \begin{coq_eval}
@@ -404,7 +404,7 @@ proof.
 \end{coq_eval} 
 \begin{coq_example}
 Show.
-hence C. (* fails *)
+Fail hence C. (* fails *)
 \end{coq_example}
 \begin{coq_eval}
 Abort.
@@ -578,7 +578,7 @@ let P:(nat -> Prop).
 \end{coq_eval} 
 \begin{coq_example}
 Show.
-let x. (* fails because x's type is not clear *) 
+Fail let x. (* fails because x's type is not clear *)
 let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
 \end{coq_example}
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 0d628ac7e..cf83d0c72 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1155,7 +1155,7 @@ Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
 \end{coq_example*}
 But the following definition will give an error:
 \begin{coq_example}
-Inductive listw (A:Set) : Set :=
+Fail Inductive listw (A:Set) : Set :=
   | nilw : listw (A*A)
   | consw : A -> listw (A*A) -> listw (A*A).
 \end{coq_example}
@@ -1401,11 +1401,11 @@ error message:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(*********      Error: Recursive call to wrongplus ...      **********)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (*********      Error: Recursive call to wrongplus ...      **********)
 \begin{coq_example}
-Fixpoint wrongplus (n m:nat) {struct n} : nat :=
+Fail Fixpoint wrongplus (n m:nat) {struct n} : nat :=
   match m with
   | O => n
   | S p => S (wrongplus n p)
@@ -1530,11 +1530,11 @@ function does not satisfy the guard condition:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(***************** Error: Unguarded recursive call *******************)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (***************** Error: Unguarded recursive call *******************)
 \begin{coq_example}
-CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
+Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
   if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
 \end{coq_example}
 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index f48cf6abf..48b9315e3 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -238,14 +238,14 @@ as the body of \texttt{x}.
 
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(***************** Error: N.y not a defined object *******************)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (***************** Error: N.y not a defined object *******************)
 \begin{coq_example}
 Module N  :  SIG with Definition T := nat  :=  M.
 Print N.T.
 Print N.x.
-Print N.y.
+Fail Print N.y.
 \end{coq_example}
 \begin{coq_eval}
 Reset N.
@@ -353,15 +353,11 @@ Example:
 
 \begin{coq_example}
 Module Mod.
-\end{coq_example}
-\begin{coq_example}
   Definition T:=nat.
   Check T.
-\end{coq_example}
-\begin{coq_example}
 End Mod.
 Check Mod.T.
-Check T. (* Incorrect ! *)
+Fail Check T. (* Incorrect! *)
 Import Mod.
 Check T. (* Now correct *)
 \end{coq_example}
@@ -386,7 +382,7 @@ Local Definition T := nat.
 End B.
 End A.
 Import A.
-Check B.T.
+Fail Check B.T.
 \end{coq_example}
 
 \begin{Variants}
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 15ddf6261..107b98f01 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -434,7 +434,7 @@ notation are replaced by ``\_''.
 \Example
 \begin{coq_example}
 Locate "exists".
-Locate "'exists' _ , _".
+Locate "exists _ .. _ , _".
 \end{coq_example}
 
 \SeeAlso Section \ref{Locate}.
@@ -516,11 +516,11 @@ the next command fails because {\tt p} does not bind in
 the instance of {\tt n}.
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following produces **********)
-(**** The reference p was not found in the current environment ********)
 \end{coq_eval}
+% (********** The following produces **********)
+% (**** The reference p was not found in the current environment ********)
 \begin{coq_example}
-Check (exists_different p).
+Fail Check (exists_different p).
 \end{coq_example}
 
 \Rem Binding variables must not necessarily be parsed using the
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c3d8ad531..52f32d0c7 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -343,7 +343,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
   This behaves like {\tt apply} but it reasons modulo conversion only
   on subterms that contain no variables to instantiate. For instance,
   the following example does not succeed because it would require the
-  conversion of {\tt id ?1234} and {\tt O}.
+  conversion of {\tt id ?foo} and {\tt O}.
 
 \begin{coq_eval}
 Reset Initial.
@@ -354,7 +354,7 @@ Hypothesis H : forall y, id y = y.
 Goal O = O.
 \end{coq_example*}
 \begin{coq_example}
-simple apply H.
+Fail simple apply H.
 \end{coq_example}
 
   Because it reasons modulo a limited amount of conversion, {\tt
@@ -419,7 +419,7 @@ no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}:
 %(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
 %\end{coq_eval}
 \begin{coq_example}
-apply Rtrans.
+Fail apply Rtrans.
 \end{coq_example}
 
 A solution is to apply {\tt (Rtrans n m p)} or {\tt (Rtrans n m)}.
@@ -914,10 +914,10 @@ containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
 \begin{coq_example}
 Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
 intros * [a | (_,c)] f.
-apply (f a).
-exact c.
-Qed.
 \end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 
 \Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
 \texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
@@ -935,7 +935,7 @@ Qed.
 Goal forall n:nat, n = 0 -> n = 0.
 intros [ | ] H.
 Show 2.
-Undo 2.
+Undo.
 intros [ | ]; intros H.
 Show 2.
 \end{coq_example}