*** empty log message ***

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

4 files changed, 29 insertions, 26 deletions

diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 6c3838080..791de51eb 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -651,11 +651,10 @@ 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:
-% (********** The following is not correct and should produce **********)
-% (********* Error: The 1st argument of list' must be A in ... *********)
-% (* Just to adjust the prompt: *) 
 \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}
 \begin{coq_example}
 Inductive list' (A:Set) : Set :=
@@ -813,12 +812,12 @@ The following declaration introduces the second-order existential
 quantifier $\exists X.P(X)$.
 \begin{coq_example*}
 Inductive exProp (P:Prop->Prop) : Prop 
-  := exP_intro : forall X:Prop, (P X) -> (exProp P).
+  := exP_intro : forall X:Prop, P X -> exProp P.
 \end{coq_example*}
 The same definition on \Set{} is not allowed and fails~:
 \begin{coq_example}
 Inductive exSet (P:Set->Prop) : Set 
-  := exS_intro : forall X:Set, (P X) -> (exSet P).
+  := exS_intro : forall X:Set, P X -> exSet P.
 \end{coq_example}
 It is possible to declare the same inductive definition in the
 universe \Type. 
@@ -826,7 +825,7 @@ The \texttt{exType} inductive definition has type  $(\Type_i \ra\Prop)\ra
 \Type_j$ with the constraint $i<j$.
 \begin{coq_example*}
 Inductive exType (P:Type->Prop) : Type
-  := exT_intro : forall X:Type, (P X) -> (exType P).
+  := exT_intro : forall X:Type, P X -> exType P.
 \end{coq_example*}
 %We shall assume for the following definitions that, if necessary, we
 %annotated the type of constructors such that we know if the argument
@@ -1002,13 +1001,17 @@ Assume $A$ and $B$ are two propositions, and the logical disjunction
 $A\vee B$ is defined inductively by~:
 \begin{coq_example*}
 Inductive or (A B:Prop) : Prop :=
-  lintro : A -> (or A B) | rintro : B -> (or A B).
+  lintro : A -> or A B | rintro : B -> or A B.
 \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}
 \begin{coq_example}
-Definition choice (A B :Prop) (x:or A B) := 
-   match x with (lintro a) => true | (rintro b) => false end.
+Definition choice (A B: Prop) (x:or A B) := 
+   match x with lintro a => true | rintro 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
@@ -1328,14 +1331,12 @@ Abort.
 \end{coq_example}
 But assuming the definition of a son function from \tree\ to \forest:
 \begin{coq_example}
-Definition sont (t:
-                   tree) : forest := let (f) := t in f.
+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_example}
 Goal forall t:tree, sizet t = S (sizef (sont t)).
-
-(** this one fails **)reflexivity.
+(** this one fails **) reflexivity.
 destruct t.
 reflexivity.
 \end{coq_example}
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 73250efd3..c486be344 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -1201,10 +1201,10 @@ error message:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example}
 (********** The following is not correct and should produce **********)
 (*********      Error: Recursive call to wrongplus ...      **********)
+\end{coq_eval}
+\begin{coq_example}
 Fixpoint wrongplus (n m:nat) {struct n} : nat :=
   match m with
   | O => n
@@ -1317,10 +1317,10 @@ function does not satisfy the guard condition:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example*}
 (********** The following is not correct and should produce **********)
 (***************** Error: Unguarded recursive call *******************)
+\end{coq_eval}
+\begin{coq_example*}
 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-lib.tex b/doc/RefMan-lib.tex
index 0d8702315..a8aefe781 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -141,10 +141,10 @@ First, we find propositional calculus connectives:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example*}
 (********** Next parsing errors for /\ and \/ are harmless ***********)
 (******************* since output is not displayed *******************)
+\end{coq_eval}
+\begin{coq_example*}
 Inductive True : Prop := I.
 Inductive False :  Prop := .
 Definition not (A: Prop) := A -> False.
@@ -161,14 +161,14 @@ Abort All.
 \ttindex{or\_introl}
 \ttindex{or\_intror}
 \ttindex{iff}
-\ttindex{IF}
+\ttindex{IF_then_else}
 \begin{coq_example*}
 End Projections.
 Inductive or (A B:Prop) : Prop :=
   | or_introl (_:A)
   | or_intror (_:B).
 Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
-Definition IF (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
+Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 \end{coq_example*}
 
 \subsubsection{Quantifiers} \label{Quantifiers}
@@ -188,7 +188,7 @@ Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
 Inductive ex (A: Set) (P:A -> Prop) : Prop :=
     ex_intro (x:A) (_:P x).
 Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
-    ex_intro2 : (x:A) (_:P x) (_:Q x).
+    ex_intro2 (x:A) (_:P x) (_:Q x).
 \end{coq_example*}
 
 The following abbreviations are allowed:
@@ -389,7 +389,7 @@ provided.
 \begin{coq_example*}
 Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
 Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
-  exist2 : (x:A) (_:P x) (_:Q x).
+  exist2 (x:A) (_:P x) (_:Q x).
 \end{coq_example*}
 
 A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined,
@@ -412,10 +412,12 @@ Variable A : Set.
 Variable P : A -> Set.
 Definition projS1 (H:sigS A P) := let (x, h) := H in x.
 Definition projS2 (H:sigS A P) :=
-  let (x, h) return P (projS1 H) := H in h.
+  match H return P (projS1 H) with
+    existS x h => h
+  end.
 End sigSprojections.
 Inductive sigS2 (A: Set) (P Q:A -> Set) : Set :=
-    existS2 : (x:A) (_:P x) (_:Q x).
+    existS2 (x:A) (_:P x) (_:Q x).
 \end{coq_example*}
 
 A related non-dependent construct is the constructive sum
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index b4cd2c9dd..29dcfa741 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1822,7 +1822,7 @@ As a consequence, {\tt eauto} can solve such a goal:
 
 \begin{coq_example}
 Hints Resolve ex_intro.
-Goal forall P:nat -> Prop, P 0 ->  EX n : _ | P n.
+Goal forall P:nat -> Prop, P 0 ->  exists n, P n.
 eauto.
 \end{coq_example}
 \begin{coq_eval}