passage V8

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

4 files changed, 464 insertions, 343 deletions

diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 5b80e4e19..704c6a618 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -594,17 +594,24 @@ The declaration for a mutual inductive definition of forests and trees is:
 These representations are the ones obtained as the result of the \Coq\ 
 declaration:
 \begin{coq_example*}
-Inductive Set nat := O : nat | S : nat -> nat.
-Inductive list [A : Set] : Set := 
-     nil : (list A) | cons : A -> (list A) -> (list A).
+Inductive nat : Set :=
+  | O : nat
+  | S : nat -> nat.
+Inductive list (A:Set) : Set :=
+  | nil : list A
+  | cons : A -> list A -> list A.
 \end{coq_example*}
 \begin{coq_example*}
-Inductive Length [A:Set] : (list A) -> nat -> Prop :=
-    Lnil : (Length A (nil A) O)
- | Lcons : (a:A)(l:(list A))(n:nat)
-           (Length A l n)->(Length A (cons A a l) (S n)).
-Mutual Inductive tree : Set := node : forest -> tree
-with forest : Set := emptyf : forest | consf : tree -> forest -> forest.
+Inductive Length (A:Set) : list A -> nat -> Prop :=
+  | Lnil : Length A (nil A) O
+  | Lcons :
+      forall (a:A) (l:list A) (n:nat),
+        Length A l n -> Length A (cons A a l) (S n).
+Inductive tree : Set :=
+    node : forest -> tree
+with forest : Set :=
+  | emptyf : forest
+  | consf : tree -> forest -> forest.
 \end{coq_example*}
 The inductive declaration in \Coq\ is slightly different from the one
 we described theoretically. The difference is that in the type of
@@ -614,14 +621,16 @@ 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}
-(********** 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.
+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).
+Inductive list' (A:Set) : Set :=
+  | nil' : list' A
+  | cons' : A -> list' (A -> A) -> list' A.
 \end{coq_example}
 
 \subsection{Types of inductive objects}
@@ -1153,16 +1162,24 @@ The following definitions are correct, we enter them using the
 {\tt Fixpoint} command as described in section~\ref{Fixpoint} and show
 the internal representation.
 \begin{coq_example}
-Fixpoint plus [n:nat] : nat -> nat :=
- [m:nat]Case n of m [p:nat](S (plus p m)) end.
+Fixpoint plus (n m:nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (plus p m)
+  end.
 Print plus.
-Fixpoint lgth [A:Set;l:(list A)] : nat :=
-  Case l of O [a:A][l':(list A)](S (lgth A l')) end.
+Fixpoint lgth (A:Set) (l:list A) {struct l} : nat :=
+  match l with
+  | nil => O
+  | cons a l' => S (lgth A l')
+  end.
 Print lgth.
-Fixpoint sizet [t:tree] : nat 
-  := Case t of [f:forest](S (sizef f)) end
-with     sizef [f:forest] : nat 
-  := Case f of O [t:tree][f:forest](plus (sizet t) (sizef f)) end.
+Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f)
+ with sizef (f:forest) : nat :=
+  match f with
+  | emptyf => O
+  | consf t f => plus (sizet t) (sizef f)
+  end.
 Print sizet.
 \end{coq_example}
 
@@ -1180,24 +1197,25 @@ and corresponds to the reduction for primitive recursive operators.
 
 We can illustrate this behavior on examples.
 \begin{coq_example}
-Goal (n,m:nat)(plus (S n) m)=(S (plus n m)).
-Reflexivity.
+Goal forall n m:nat, plus (S n) m = S (plus n m).
+reflexivity.
 Abort.
-Goal (f:forest)(sizet (node f))=(S (sizef f)).
-Reflexivity.
+Goal forall f:forest, sizet (node f) = S (sizef f).
+reflexivity.
 Abort.
 \end{coq_example}
 But assuming the definition of a son function from \tree\ to \forest:
 \begin{coq_example}
-  Definition sont : tree -> forest := [t]Case t of [f]f end.
+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 (t:tree)(sizet t)=(S (sizef (sont t))).
-(** this one fails **)
-Reflexivity.
-Destruct t.
-Reflexivity.
+Goal forall t:tree, sizet t = S (sizef (sont t)).
+
+(** this one fails **)reflexivity.
+olddestruct t.
+reflexivity.
 \end{coq_example}
 \begin{coq_eval}
 Abort.
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index e5f908a0c..1fb256596 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -66,12 +66,13 @@ The set of rational numbers may be defined as:
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Record Rat : Set := mkRat {
- sign     : bool;
- top      : nat;
- bottom   : nat;
- Rat_bottom_cond : ~O=bottom;
- Rat_irred_cond:(x,y,z:nat)(mult x y)=top/\(mult x z)=bottom->x=(S O)}.
+Record Rat : Set := mkRat
+  {sign : bool;
+   top : nat;
+   bottom : nat;
+   Rat_bottom_cond : 0%N <> bottom;
+   Rat_irred_cond :
+    forall x y z:nat, (x * y)%N = top /\ (x * z)%N = bottom -> x = 1%N}.
 \end{coq_example}
 
 Remark here that the field
@@ -95,37 +96,39 @@ the record.
 Let us define the rational $1/2$.
 
 \begin{coq_example*}
-Require Arith.
-Theorem one_two_irred: (x,y,z:nat)(mult x y)=(1)/\(mult x z)=(2)->x=(1).
+Require Import Arith.
+Theorem one_two_irred :
+ forall x y z:nat, (x * y)%N = 1%N /\ (x * z)%N = 2%N -> x = 1%N.
 \end{coq_example*}
 \begin{coq_eval}
-Lemma plus_m_n_eq_n_O : (m,n:nat)(plus m n)=O -> n=O.
-Destruct m; Trivial.
-Intros; Discriminate.
+Lemma plus_m_n_eq_n_O : forall m n:nat, (m + n)%N = 0%N -> n = 0%N.
+olddestruct m; trivial.
+intros; discriminate.
 Qed.
-
-Lemma mult_m_n_eq_m_1: (m,n:nat)(mult m n)=((S O))->m=(S O).
-Destruct m;Trivial.
-Intros; Apply f_equal with f:=S.
-Generalize H.
-Case n; Trivial.
-Simpl.
-Case n0;Simpl.
-Intro; Rewrite <- mult_n_O; Intro; Discriminate.
-Intros n1 n2 H0; Injection H0.
-Intro H1.
-LetTac H2:=(plus_m_n_eq_n_O n1 (S (plus n1 (mult n2 (S n1)))) H1).
-Discriminate.
+Lemma mult_m_n_eq_m_1 : 
+ forall m n:nat, (m * n)%N = 1%N -> m = 1%N.
+olddestruct m; trivial.
+intros; apply f_equal with (f := S).
+generalize H.
+case n; trivial.
+simpl.
+case n0; simpl.
+intro; rewrite <- mult_n_O; intro; discriminate.
+intros n1 n2 H0; injection H0.
+intro H1.
+lettac H2 := (plus_m_n_eq_n_O n1 (S (n1 + n2 * S n1)) H1).
+discriminate.
 Qed.
 
-Intros x y z (H1,H2). Apply mult_m_n_eq_m_1 with n:=y; Trivial.
+intros x y z [H1 H2].
+ apply mult_m_n_eq_m_1 with (n := y); trivial.
 \end{coq_eval}
 \ldots
 \begin{coq_example*}
 Qed.
 \end{coq_example*}
 \begin{coq_example}
-Definition half := (mkRat true (1) (2) (O_S (1)) one_two_irred).
+Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
 \end{coq_example}
 \begin{coq_example}
 Check half.
@@ -138,9 +141,9 @@ fields. If a field is named ``\verb=_='' then no projection is built for
 this (anonymous) field. In our example:
 
 \begin{coq_example}
-Eval Compute in (top half).
-Eval Compute in (bottom half).
-Eval Compute in (Rat_bottom_cond half).
+Eval compute in half.(top).
+Eval compute in half.(bottom).
+Eval compute in half.(Rat_bottom_cond).
 \end{coq_example}
 \begin{coq_eval}
 Reset Initial.
@@ -241,7 +244,11 @@ term & ::= & \zeroone{\annotation} {\tt if} {\term} {\tt then} {\term} {\tt else
 For instance, the definition
 
 \begin{coq_example}
-Definition not := [b:bool] Cases b of true => false | false => true end.
+Definition not (b:bool) :=
+  match b with
+  | true => false
+  | false => true
+  end.
 \end{coq_example}
 
 can be alternatively written
@@ -250,7 +257,7 @@ can be alternatively written
 Reset not.
 \end{coq_eval}
 \begin{coq_example}
-Definition not := [b:bool] if b then false else true.
+Definition not (b:bool) := if b then false else true.
 \end{coq_example}
 
 \subsection{Irrefutable patterns: the destructuring {\tt let}}
@@ -271,7 +278,9 @@ This enriches the syntax of terms as follows:
 For instance, the definition
 
 \begin{coq_example}
-Definition fst := [A,B:Set][H:A*B] Cases H of (pair x y) => x end.
+Definition fst (A B:Set) (H:A * B) := match H with
+                                      | pair x y => x
+                                      end.
 \end{coq_example}
 
 can be alternatively written 
@@ -280,7 +289,7 @@ can be alternatively written
 Reset fst.
 \end{coq_eval}
 \begin{coq_example}
-Definition fst := [A,B:Set][p:A*B] let (x,_) = p in x.
+Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x.
 \end{coq_example}
 
 The pretty-printing of a definition by cases on a irrefutable pattern
@@ -458,8 +467,8 @@ the variables involved in the term.
 Example:
 
 \begin{coq_example}
-Definition ID := (X:Set) X -> X.
-Definition id := (([X][x]x) :: ID).
+Definition ID := forall X:Set, X -> X.
+Definition id := (fun X x => x):ID.
 Check id.
 \end{coq_example}
 
@@ -490,9 +499,9 @@ substituted in the other definitions.
 Here is an example :
 \begin{coq_example}
 Section s1.
-Variables x,y : nat.
+Variables x y : nat.
 Local y' := y.
-Definition x' := (S x).
+Definition x' := S x.
 Print x'.
 End s1.
 Print x'.
@@ -636,9 +645,9 @@ Reset Initial.
 \end{coq_eval}
 
 \begin{coq_example}
-Check O.
+Check 0%N.
 Definition nat := bool.
-Check O.
+Check 0%N.
 Check Datatypes.nat.
 \end{coq_example}
 
@@ -709,15 +718,15 @@ correspond respectively to the positions {\tt 1}, {\tt 2} and {\tt 4}.
 Set Implicit Arguments.
 Variable X : Type.
 Definition Relation := X -> X -> Prop.
-Definition Transitivity := [R:Relation]
-           (x,y:X)(R x y) -> (z:X)(R y z) -> (R x z).
-Variables R:Relation; p:(Transitivity R).
+Definition Transitivity (R:Relation) :=
+  forall x y:X, R x y -> forall z:X, R y z -> R x z.
+Variables (R : Relation) (p : Transitivity R).
 \end{coq_example*}
 \begin{coq_example}
 Print p.
 \end{coq_example}
 \begin{coq_example*}
-Variables a,b,c:X;  r1:(R a b); r2:(R b c).
+Variables (a b c : X) (r1 : R a b) (r2 : R b c).
 \end{coq_example*}
 \begin{coq_example}
 Check (p r1 r2).
@@ -743,8 +752,8 @@ also give all the arguments of an application, we have then to write
 \Example
 
 \begin{coq_example}
-Check (p r1 4!c).
-Check (!p a b r1 c r2).
+Check (p r1 (z:=c)).
+Check (p (x:=a) (y:=b) r1 (z:=c) r2).
 \end{coq_example}
 
 \subsubsection{Implicit Arguments and Pretty-Printing}
@@ -774,18 +783,18 @@ Let us extend our functional language with the definition of the
 identity function:
 
 \begin{coq_eval}
-Unset Implicit Arguments.
+Set Strict Implicit.
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Definition explicit_id := [A:Set][a:A]a.
+Definition explicit_id (A:Set) (a:A) := a.
 \end{coq_example}
 
 \index{questionmark@{\texttt{?}}}
 We declare also a syntactic definition {\tt id}:
 
 \begin{coq_example}
-Syntactic Definition id := (explicit_id ?).
+Notation id := (explicit_id _).
 \end{coq_example}
 
 The term {\tt (explicit\_id ?)} is untyped since the implicit
@@ -794,7 +803,7 @@ definition.  Let us see what happens when we use a syntactic constant
 in an expression like in the following example.
 
 \begin{coq_example}
-Check (id O).
+Check (id 0%N).
 \end{coq_example}
 
 \noindent First the syntactic constant {\tt id} is replaced by its
@@ -818,14 +827,14 @@ We can define a new syntactic definition {\tt id1} for {\tt
 syntactic constant in order to avoid a name conflict with {\tt id}.
 
 \begin{coq_example}
-Syntactic Definition id1 := explicit_id | 1.
+Notation id1 := id.
 \end{coq_example}
 
 The new syntactic constant {\tt id1} has the same behavior as {\tt
   id}:
 
 \begin{coq_example}
-Check (id1 O).
+Check (id1 0%N).
 \end{coq_example}
 
 
@@ -860,17 +869,17 @@ Canonical structures are particularly useful when mixed with
 coercions and implicit arguments. Here is an example.
 
 \begin{coq_example*}
-Require Relations.
-Require EqNat.
+Require Import Relations.
+Require Import EqNat.
 Set Implicit Arguments.
-Structure Setoid : Type :=
- {Carrier   :> Set;
-  Equal     : (relation Carrier);
-  Prf_equiv : (equivalence Carrier Equal)}.
-Definition is_law := [A,B:Setoid][f:A->B]
-  (x,y:A) (Equal x y) -> (Equal (f x) (f y)).
-Axiom eq_nat_equiv : (equivalence nat eq_nat).
-Definition nat_setoid : Setoid := (Build_Setoid eq_nat_equiv).
+Structure Setoid : Type := 
+  {Carrier :> Set;
+   Equal : relation Carrier;
+   Prf_equiv : equivalence Carrier Equal}.
+Definition is_law (A B:Setoid) (f:A -> B) :=
+  forall x y:A, _.(@Equal) x y -> _.(@Equal) (f x) (f y).
+Axiom eq_nat_equiv : equivalence nat eq_nat.
+Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
 Canonical Structure nat_setoid.
 \end{coq_example*}
 
@@ -878,7 +887,7 @@ Thanks to \texttt{nat\_setoid} declared as canonical, the implicit
 arguments {\tt A} and {\tt B} can be synthesized in the next statement.
 
 \begin{coq_example}
-Lemma is_law_S : (is_law S).
+Lemma is_law_S : is_law (A:=_) (B:=_) S.
 \end{coq_example}
 
 \Rem If a same field occurs in several canonical structure, then
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 1b23911dd..2e643e470 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -735,7 +735,9 @@ two examples of the use of the {\tt Inductive} definitions.
 
 The set of natural numbers is defined as:
 \begin{coq_example}
-Inductive nat : Set := O : nat | S : nat -> nat.
+Inductive nat : Set :=
+  | O : nat
+  | S : nat -> nat.
 \end{coq_example}
 
 The type {\tt nat} is defined as the least \verb:Set: containing {\tt
@@ -772,9 +774,9 @@ As an example of annotated inductive types, let us define the
 $even$ predicate:
 
 \begin{coq_example}
-Inductive even : nat->Prop :=
- | even_0  : (even O)
- | even_SS : (n:nat)(even n)->(even (S (S n))).
+Inductive even : nat -> Prop :=
+  | even_0 : even O
+  | even_SS : forall n:nat, even n -> even (S (S n)).
 \end{coq_example}
 
 The type {\tt nat->Prop} means that {\tt even} is a unary predicate
@@ -807,8 +809,9 @@ induction principle we got for {\tt nat}.
   For instance, one can define
   parameterized lists as:
 \begin{coq_example*}
-Inductive list [X:Set] : Set :=
- Nil : (list X) | Cons : X->(list X)->(list X).
+Inductive list (X:Set) : Set :=
+  | Nil : list X
+  | Cons : X -> list X -> list X.
 \end{coq_example*}
 Notice that, in the type of {\tt Nil} and {\tt Cons}, we write {\tt
   (list X)} and not just {\tt list}.\\ The constants {\tt Nil} and
@@ -899,11 +902,12 @@ trees and forests. We assume given two types $A$ and $B$ as variables.
 It can be declared the following way.
 
 \begin{coq_example*}
-Variables A,B:Set.
-Inductive tree : Set :=  node : A -> forest -> tree
-with forest : Set := 
-   | leaf : B -> forest 
-   | cons : tree -> forest -> forest.
+Variables A B : Set.
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | leaf : B -> forest
+  | cons : tree -> forest -> forest.
 \end{coq_example*}
 
 This declaration generates automatically six induction
@@ -930,10 +934,11 @@ following way:
 Reset tree.
 \end{coq_eval}
 \begin{coq_example*}
-Inductive
-     tree   [A,B:Set] : Set := node : A -> (forest A B) -> (tree A B)
-with forest [A,B:Set] : Set := leaf : B -> (forest A B)
-                   | cons : (tree A B) -> (forest A B) -> (forest A B).
+Inductive tree (A B:Set) : Set :=
+    node : A -> forest A B -> tree A B
+with forest (A B:Set) : Set :=
+  | leaf : B -> forest A B
+  | cons : tree A B -> forest A B -> forest A B.
 \end{coq_example*}
 
 Assume we define an inductive definition inside a section.  When the
@@ -958,7 +963,8 @@ An example of a co-inductive type is the type of infinite sequences of
 natural numbers, usually called streams. It can be introduced in \Coq\
 using the \texttt{CoInductive} command:
 \begin{coq_example}
-CoInductive Set Stream  := Seq : nat->Stream->Stream.
+CoInductive Stream : Set :=
+    Seq : nat -> Stream -> Stream.
 \end{coq_example}
 
 The syntax of this command is the same as the command \texttt{Inductive}
@@ -970,8 +976,12 @@ analysis. For example, the usual destructors on streams
 \texttt{hd:Stream->nat} and \texttt{tl:Str->Str} can be defined as
 follows:
 \begin{coq_example}
-Definition hd  := [x:Stream]Cases x of (Seq a s) => a  end.
-Definition tl  := [x:Stream]Cases x of (Seq a s) => s  end.
+Definition hd (x:Stream) := match x with
+                            | Seq a s => a
+                            end.
+Definition tl (x:Stream) := match x with
+                            | Seq a s => s
+                            end.
 \end{coq_example}
 
 Definition of co-inductive predicates and blocks of mutually
@@ -979,10 +989,10 @@ co-inductive definitions are also allowed. An example of a
 co-inductive predicate is the extensional equality on streams:
 
 \begin{coq_example}
-CoInductive EqSt  : Stream->Stream->Prop := 
-            eqst : (s1,s2:Stream)
-                    (hd s1)=(hd s2)->
-                     (EqSt (tl s1) (tl s2))->(EqSt s1 s2).
+CoInductive EqSt : Stream -> Stream -> Prop :=
+    eqst :
+      forall s1 s2:Stream,
+        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
 \end{coq_example}
 
 In order to prove the extensionally equality of two streams $s_1$ and
@@ -1012,8 +1022,11 @@ ensure that the {\tt Fixpoint} definition always terminates. For
 instance, one can define the addition function as :
 
 \begin{coq_example}
-Fixpoint add [n:nat] : nat->nat 
-   := [m:nat]Cases n of O => m | (S p) => (S (add p m)) end.
+Fixpoint add (n m:nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (add p m)
+  end.
 \end{coq_example}
 
 The {\tt Cases} operator matches a value (here \verb:n:) with the
@@ -1048,13 +1061,19 @@ decreases because it is a {\em pattern variable} coming from {\tt Cases
 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.
+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.
+Fixpoint wrongplus
+ (n
+  
+  (********** The following is not correct and should produce **********)
+  (********* Error: Recursive call applied to an illegal term **********)
+  (* Just to adjust the prompt: *) m:nat) {struct n} : nat :=
+  match m with
+  | O => n
+  | S p => S (wrongplus n p)
+  end.
 \end{coq_example}
 
 because the declared decreasing argument {\tt n} actually does not
@@ -1062,26 +1081,35 @@ decrease in the recursive call.  The function computing the addition
 over the second argument should rather be written:
 
 \begin{coq_example*}
-Fixpoint plus [n,m:nat] : nat 
-   := Cases m of O => n | (S p) => (S (plus n p)) end.
+Fixpoint plus (n m:nat) {struct m} : nat :=
+  match m with
+  | O => n
+  | S p => S (plus n p)
+  end.
 \end{coq_example*}
 
 The ordinary match operation on natural numbers can be mimicked in the
 following way.
 \begin{coq_example*}
-Fixpoint nat_match [C:Set;f0:C;fS:nat->C->C;n:nat] : C 
-   := Cases n of O => f0 | (S p) => (fS p (nat_match C f0 fS p)) end.
+Fixpoint nat_match (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n}
+ : C := match n with
+        | O => f0
+        | S p => fS p (nat_match C f0 fS p)
+        end.
 \end{coq_example*}
 The recursive call may not only be on direct subterms of the recursive
 variable {\tt n} but also on a deeper subterm and we can directly
 write the function {\tt mod2} which gives the remainder modulo 2 of a
 natural number.
 \begin{coq_example*}
-Fixpoint mod2 [n:nat] : nat
-   := Cases n of
-         O    => O
-      | (S p) => Cases p of O => (S O) | (S q) => (mod2 q) end
-      end.
+Fixpoint mod2 (n:nat) : nat :=
+  match n with
+  | O => O
+  | S p => match p with
+           | O => S O
+           | S q => mod2 q
+           end
+  end.
 \end{coq_example*}
 In order to keep the strong normalisation property, the fixed point
 reduction will only be performed when the argument in position of the
@@ -1096,18 +1124,23 @@ generally any mutually recursive definitions.
 The size of trees and forests can be defined the following way: 
 \begin{coq_eval}
 Reset Initial.
-Variables A,B:Set.
-Inductive tree : Set :=  node : A -> forest -> tree
-with forest : Set := leaf : B -> forest 
-                   | cons : tree -> forest -> forest.
+Variables A B : Set.
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | leaf : B -> forest
+  | cons : tree -> forest -> forest.
 \end{coq_eval}
 \begin{coq_example*}
-Fixpoint tree_size [t:tree] : nat :=
-    Cases t of (node a f) => (S (forest_size f)) end
-with forest_size [f:forest] : nat := 
-    Cases f of (leaf b) => (S O)
-          | (cons t f') => (plus (tree_size t) (forest_size f')) 
-         end.
+Fixpoint tree_size (t:tree) : nat :=
+  match t with
+  | node a f => S (forest_size f)
+  end
+ with forest_size (f:forest) : nat :=
+  match f with
+  | leaf b => 1%N
+  | cons t f' => (tree_size t + forest_size f')%N
+  end.
 \end{coq_example*}
 A generic command {\tt Scheme} is useful to build automatically various
 mutual induction principles. It is described in section \ref{Scheme}.
@@ -1121,12 +1154,17 @@ containing all natural numbers can be introduced applying the
 following method to the number \texttt{O}:
 
 \begin{coq_example*}
-CoInductive Set Stream  := Seq : nat->Stream->Stream.
-Definition hd  := [x:Stream]Cases x of (Seq a s) => a  end.
-Definition tl  := [x:Stream]Cases x of (Seq a s) => s  end.
+CoInductive Stream : Set :=
+    Seq : nat -> Stream -> Stream.
+Definition hd (x:Stream) := match x with
+                            | Seq a s => a
+                            end.
+Definition tl (x:Stream) := match x with
+                            | Seq a s => s
+                            end.
 \end{coq_example*}
 \begin{coq_example}
-CoFixpoint from  : nat->Stream := [n:nat](Seq n (from (S n))).
+CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
 \end{coq_example}
 
 Oppositely to recursive ones, there is no decreasing argument in a
@@ -1141,16 +1179,16 @@ 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.
+Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example*}
-CoFixpoint filter  : (nat->bool)->Stream->Stream := 
-   [p:nat->bool]
-     [s:Stream]
-       if (p (hd s)) then (Seq (hd s) (filter p (tl s)))
-       else (filter p (tl s)).
+CoFixpoint filter
+ (
+  (********** The following is not correct and should produce **********)
+  (***************** Error: Unguarded recursive call *******************)
+  (* Just to adjust the prompt: *) 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*}
 
 \noindent Notice that the definition contains an unguarded recursive
@@ -1164,9 +1202,9 @@ evaluated. We can test this using the command \texttt{Eval},
 which computes the normal forms of a term:
 
 \begin{coq_example}
-Eval Compute in (from O).
-Eval Compute in (hd (from O)).
-Eval Compute in (tl (from O)).  
+Eval compute in (from 0).
+Eval compute in (hd (from 0)).
+Eval compute in (tl (from 0)).
 \end{coq_example}
 
 As in the \texttt{Fixpoint} command (cf. section~\ref{Fixpoint}), it
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 5d743e0e7..88cbbc57d 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -102,19 +102,23 @@ First, we find propositional calculus connectives:
 \ttindex{proj2}
 
 \begin{coq_eval}
-(********** Next parsing errors for /\ and \/ are harmless ***********)
-(******************* since output is not displayed *******************)
-(* Just to adjust the prompt: *) Set Printing Depth 50.
+Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example*}
-Inductive True : Prop := I : True. 
-Inductive False : Prop := . 
-Definition not := [A:Prop] A->False.
-Inductive and [A,B:Prop] : Prop := conj : A -> B -> A/\B.
+Inductive True :
+
+(********** Next parsing errors for /\ and \/ are harmless ***********)
+(******************* since output is not displayed *******************)
+(* Just to adjust the prompt: *) Prop :=
+    I : True.
+Inductive False :  Prop :=.
+Definition not (A: Prop) := A -> False.
+Inductive and (A B:Prop) : Prop :=
+    conj : A -> B -> A /\ B.
 Section Projections.
-Variables A,B : Prop.
-Theorem proj1 : A/\B -> A.
-Theorem proj2 : A/\B -> B.
+Variables A B : Prop.
+Theorem proj1 : A /\ B -> A.
+Theorem proj2 : A /\ B -> B.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
@@ -126,11 +130,11 @@ Abort All.
 \ttindex{IF}
 \begin{coq_example*}
 End Projections.
-Inductive or [A,B:Prop] : Prop
-    := or_introl : A -> A\/B 
-     | or_intror : B -> A\/B.
-Definition iff := [P,Q:Prop] (P->Q) /\ (Q->P).
-Definition IF := [P,Q,R:Prop] (P/\Q) \/ (~P/\R).
+Inductive or (A B:Prop) : Prop :=
+  | or_introl : A -> A \/ B
+  | or_intror : B -> A \/ B.
+Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
+Definition IF (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 \end{coq_example*}
 
 \subsubsection{Quantifiers} \label{Quantifiers}
@@ -148,11 +152,11 @@ Then we find first-order quantifiers:
 \ttindex{ex\_intro2}
 
 \begin{coq_example*}
-Definition all := [A:Set][P:A->Prop](x:A)(P x). 
-Inductive ex [A:Set;P:A->Prop] : Prop 
-    := ex_intro : (x:A)(P x)->(ex A P).
-Inductive ex2 [A:Set;P,Q:A->Prop] : Prop
-    := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q).
+Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
+Inductive ex (A: Set) (P:A -> Prop) : Prop :=
+    ex_intro : forall x:A, P x -> ex A P.
+Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
+    ex_intro2 : forall x:A, P x -> Q x -> ex2 A P Q.
 \end{coq_example*}
 
 The following abbreviations are allowed:
@@ -186,8 +190,8 @@ equivalent to Leibniz' equality.
 \ttindex{refl\_equal}
 
 \begin{coq_example*}
-Inductive eq [A:Set;x:A] : A->Prop
-    := refl_equal : (eq A x x).
+Inductive eq (A:Set) (x:A) : A -> Prop :=
+    refl_equal : eq A x x.
 \end{coq_example*}
 
 \subsubsection{Lemmas} \label{PreludeLemmas}
@@ -196,7 +200,7 @@ Finally, a few easy lemmas are provided.
 \ttindex{absurd}
 
 \begin{coq_example*}
-Theorem absurd : (A:Prop)(C:Prop) A -> ~A -> C.
+Theorem absurd : forall A C:Prop, A -> ~ A -> C.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -207,13 +211,20 @@ Abort.
 \ttindex{sym\_not\_eq}
 \begin{coq_example*}
 Section equality.
- Variable A,B : Set.
- Variable f   : A->B.
- Variable x,y,z : A.
- Theorem sym_eq : x=y -> y=x.
- Theorem trans_eq : x=y -> y=z -> x=z.
- Theorem f_equal : x=y -> (f x)=(f y).
- Theorem sym_not_eq : ~(x=y) -> ~(y=x).
+Variables A B : 
+             Set.
+Variable f : 
+            A -> B.
+Variables x y z : 
+             A.
+Theorem sym_eq : 
+  x = y -> y = x.
+Theorem trans_eq : 
+  x = y -> y = z -> x = z.
+Theorem f_equal : 
+  x = y -> f x = f y.
+Theorem sym_not_eq : 
+  x <> y -> y <> x.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -228,9 +239,12 @@ Abort.
 %Definition eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(x=y)->(P y).
 \begin{coq_example*}
 End equality.
-Definition eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)(y=x)->(P y).
-Definition eq_rec_r : (A:Set)(x:A)(P:A->Set)(P x)->(y:A)(y=x)->(P y).
-Definition eq_rect_r : (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(y=x)->(P y).
+Definition eq_ind_r :
+  forall (A:Set) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
+Definition eq_rec_r :
+  forall (A:Set) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
+Definition eq_rect_r :
+  forall (A:Set) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -248,9 +262,9 @@ arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3},
 {\tt f\_equal4} and {\tt f\_equal5}.
 For instance {\tt f\_equal3} is defined the following way.
 \begin{coq_example*}
-Theorem f_equal3 : (A1,A2,A3,B:Set)(f:A1->A2->A3->B)
-   (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)
-   (x1=y1) -> (x2=y2) -> (x3=y3)-> (f x1 x2 x3)=(f y1 y2 y3).
+Theorem f_equal3 :
+ forall (A1 A2 A3 B:Set) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2)
+   (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -282,13 +296,17 @@ again defined as inductive constructions over the sort
 \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.
+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*}
 
 Note that zero is the letter \verb:O:, and {\sl not} the numeral
@@ -311,17 +329,25 @@ We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and
 \ttindex{Snd}
 
 \begin{coq_example*}
-Inductive sum [A,B:Set] : Set
-    := inl : A -> (sum A B)
-     | inr : B -> (sum A B).
-Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B).
+Inductive sum (A B:Set) : Set :=
+  | inl : A -> sum A B
+  | inr : B -> sum A B.
+Inductive prod (A B:Set) : Set :=
+    pair : A -> B -> prod A B.
 Section projections.
-   Variables A,B:Set.
-   Definition fst := [H:(prod A B)] Cases H of (pair x y) => x end.
-   Definition snd := [H:(prod A B)] Cases H of (pair x y) => y end.
+Variables A B : 
+               Set.
+Definition fst (H:
+                   prod A B) := match H with
+                                | pair x y => x
+                                end.
+Definition snd (H:
+                   prod A B) := match H with
+                                | pair x y => y
+                                end.
 End projections.
-Syntactic Definition Fst := (fst ? ?).
-Syntactic Definition Snd := (snd ? ?).
+Notation Fst := (fst _ _).
+Notation Snd := (snd _ _).
 \end{coq_example*}
 
 \subsection{Specification}
@@ -353,10 +379,10 @@ provided.
 \ttindex{exist2}
 
 \begin{coq_example*}
-Inductive  sig [A:Set;P:A->Prop] : Set
-    := exist : (x:A)(P x) -> (sig A P).
-Inductive sig2 [A:Set;P,Q:A->Prop] : Set
-    := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q).
+Inductive sig (A:Set) (P:A -> Prop) : Set :=
+    exist : forall x:A, P x -> sig A P.
+Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
+    exist2 : forall x:A, P x -> Q x -> sig2 A P Q.
 \end{coq_example*}
 
 A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined,
@@ -373,17 +399,21 @@ constructor.
 \ttindex{existS2}
 
 \begin{coq_example*}
-Inductive sigS [A:Set;P:A->Set] : Set
-    := existS : (x:A)(P x) -> (sigS A P).
+Inductive sigS (A:Set) (P:A -> Set) : Set :=
+    existS : forall x:A, P x -> sigS A P.
 Section sigSprojections.
-   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)]<[H:(sigS A P)](P (projS1 H))>
-                            let (x,h) = H in h.
-End sigSprojections. 
-Inductive sigS2 [A:Set;P,Q:A->Set] : Set
-    := existS2 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q).
+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) as H return P (projS1 H) := H in h.
+End sigSprojections.
+Inductive sigS2 (A: Set) (P Q:A -> Set) : Set :=
+    existS2 : forall x:A, P x -> Q x -> sigS2 A P Q.
 \end{coq_example*}
 
 A related non-dependent construct is the constructive sum
@@ -395,9 +425,9 @@ A related non-dependent construct is the constructive sum
 \ttindex{\{A\}+\{B\}}
 
 \begin{coq_example*}
-Inductive sumbool [A,B:Prop] : Set
-    := left  : A -> (sumbool A B)
-     | right : B -> (sumbool A B).
+Inductive sumbool (A B:Prop) : Set :=
+  | left : A -> sumbool A B
+  | right : B -> sumbool A B.
 \end{coq_example*}
 
 This \verb"sumbool" construct may be used as a kind of indexed boolean
@@ -410,9 +440,9 @@ in the \verb"Set" \verb"A+{B}".
 \ttindex{A+\{B\}}
 
 \begin{coq_example*}
-Inductive sumor [A:Set;B:Prop] : Set
-    := inleft  : A -> (sumor A B) 
-     | inright : B -> (sumor A B) .
+Inductive sumor (A:Set) (B:Prop) : Set :=
+  | inleft : A -> sumor A B
+  | inright : B -> sumor A B.
 \end{coq_example*}
 
 \begin{figure}
@@ -448,13 +478,19 @@ Intuitionistic Type Theory.
 \ttindex{bool\_choice}
 
 \begin{coq_example*}
-Lemma Choice : (S,S':Set)(R:S->S'->Prop)((x:S){y:S'|(R x y)})
-                       -> {f:S->S'|(z:S)(R z (f z))}.
-Lemma Choice2 : (S,S':Set)(R:S->S'->Set)((x:S){y:S' & (R x y)})
-                       -> {f:S->S' & (z:S)(R z (f z))}.
-Lemma bool_choice : (S:Set)(R1,R2:S->Prop)((x:S){(R1 x)}+{(R2 x)}) ->
- {f:S->bool | (x:S)( ((f x)=true  /\ (R1 x)) 
-                  \/ ((f x)=false /\ (R2 x)))}.
+Lemma Choice :
+ forall (S S':Set) (R:S -> S' -> Prop),
+   (forall x:S, {y : S' | R x y}) ->
+   {f : S -> S' | forall z:S, R z (f z)}.
+Lemma Choice2 :
+ forall (S S':Set) (R:S -> S' -> Set),
+   (forall x:S, {y : S' &  R x y}) ->
+   {f : S -> S' &  forall z:S, R z (f z)}.
+Lemma bool_choice :
+ forall (S:Set) (R1 R2:S -> Prop),
+   (forall x:S, {R1 x} + {R2 x}) ->
+   {f : S -> bool |
+   forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -490,9 +526,10 @@ interpretation.
 %Lemma False_rect : (P:Type)False->P.
 \begin{coq_example*}
 Definition except := False_rec.
-Syntactic Definition Except := (except ?).
-Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C.
-Theorem and_rec : (A,B:Prop)(C:Set)(A->B->C)->(A/\B)->C.
+Notation Except := (except _).
+Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
+Theorem and_rec :
+ forall (A B:Prop) (C:Set), (A -> B -> C) -> A /\ B -> C.
 \end{coq_example*}
 %\begin{coq_eval}
 %Abort.
@@ -520,50 +557,57 @@ multiplication\footnote{This is in module {\tt Peano.v}}.
 \ttindex{mult\_n\_Sm}
 
 \begin{coq_example*}
-Theorem eq_S : (n,m:nat) n=m -> (S n)=(S m).
+Theorem eq_S : forall n m:nat, n = m -> S n = S m.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
 \end{coq_eval}
 \begin{coq_example*}
-Definition pred : nat->nat 
-     := [n:nat](<nat>Cases n of O => O 
-                          | (S u) => u end).
-Theorem pred_Sn : (m:nat) m=(pred (S m)).
-Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m.
+Definition pred (n:nat) : nat :=
+  match n return nat with
+  | O => O
+  | S u => u
+  end.
+Theorem pred_Sn : forall m:nat, m = pred (S m).
+Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
 Hints Immediate eq_add_S : core.
-Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)).
+Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
 \begin{coq_example*}
-Definition IsSucc : nat->Prop
-  := [n:nat](Cases n of O => False
-                  | (S p) => True end).
-Theorem O_S : (n:nat) ~(O=(S n)).
-Theorem n_Sn : (n:nat) ~(n=(S n)).
+Definition IsSucc (n:nat) : Prop :=
+  match n with
+  | O => False
+  | S p => True
+  end.
+Theorem O_S : forall n:nat, O <> S n.
+Theorem n_Sn : forall n:nat, n <> S n.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
 \begin{coq_example*}
-Fixpoint plus [n:nat] : nat -> nat := 
-   [m:nat](Cases n of 
-       O  => m 
-  | (S p) => (S (plus p m)) end).
-Lemma plus_n_O : (n:nat) n=(plus n O).
-Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
+Fixpoint plus (n m:nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (plus p m)
+  end.
+Lemma plus_n_O : forall n:nat, n = plus n O.
+Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus n (S m).
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
 \begin{coq_example*}
-Fixpoint mult [n:nat] : nat -> nat := 
-   [m:nat](Cases n of O => O 
-                | (S p) => (plus m (mult p m)) end).
-Lemma mult_n_O : (n:nat) O=(mult n O).
-Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
+Fixpoint mult (n m:nat) {struct n} : nat :=
+  match n with
+  | O => O
+  | S p => plus m (mult p m)
+  end.
+Lemma mult_n_O : forall n:nat, O = mult n O.
+Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult n (S m).
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
@@ -579,12 +623,12 @@ Finally, it gives the definition of the usual orderings \verb:le:,
 \ttindex{gt}
 
 \begin{coq_example*}
-Inductive le [n:nat] : nat -> Prop
-    := le_n : (le n n)
-     | le_S : (m:nat)(le n m)->(le n (S m)).
-Definition lt := [n,m:nat](le (S n) m).
-Definition ge := [n,m:nat](le m n).
-Definition gt := [n,m:nat](lt m n).
+Inductive le (n:nat) : nat -> Prop :=
+  | le_n : le n n
+  | le_S : forall m:nat, le n m -> le n (S m).
+Definition lt (n m:nat) := le (S n) m.
+Definition ge (n m:nat) := le m n.
+Definition gt (n m:nat) := lt m n.
 \end{coq_example*}
 
 Properties of these relations are not initially known, but may be
@@ -596,16 +640,18 @@ induction principle.
 \ttindex{nat\_double\_ind}
 
 \begin{coq_example*}
-Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
+Theorem nat_case :
+ forall (n:nat) (P:nat -> Prop), P O -> (forall m:nat, P (S m)) -> P n.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
 \begin{coq_example*}
-Theorem nat_double_ind : (R:nat->nat->Prop)
-     ((n:nat)(R O n)) -> ((n:nat)(R (S n) O))
-     -> ((n,m:nat)(R n m)->(R (S n) (S m)))
-     -> (n,m:nat)(R n m).
+Theorem nat_double_ind :
+ forall R:nat -> nat -> Prop,
+   (forall n:nat, R O n) ->
+   (forall n:nat, R (S n) O) ->
+   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
@@ -624,30 +670,36 @@ well-founded induction\footnote{This is defined in module {\tt Wf.v}}.
 \ttindex{well\_founded}
 
 \begin{coq_example*}
-Chapter Well_founded.
+Section Well_founded.
 Variable A : Set.
 Variable R : A -> A -> Prop.
-Inductive Acc : A -> Prop 
-   := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x).
-Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y).
+Inductive Acc : A -> Prop :=
+    Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
+Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
 \end{coq_example*}
 \begin{coq_eval}
-Destruct 1; Trivial.
+olddestruct 1; trivial.
 Defined.
 \end{coq_eval}
 \begin{coq_example*}
 Section AccRec.
 Variable P : A -> Set.
-Variable F : (x:A)((y:A)(R y x)->(Acc y))->((y:A)(R y x)->(P y))->(P x).
-Fixpoint Acc_rec [x:A;a:(Acc x)] : (P x)
-   := (F x (Acc_inv x a) [y:A][h:(R y x)](Acc_rec y (Acc_inv x a y h))).
+Variable
+  F :
+    forall x:A,
+      (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
+Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x :=
+  F x (Acc_inv x a)
+    (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)).
 End AccRec.
-Definition well_founded := (a:A)(Acc a).
+Definition well_founded := forall a:A, Acc a.
 Hypothesis Rwf : well_founded.
-Theorem well_founded_induction : 
-        (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
-Theorem well_founded_ind : 
-        (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
+Theorem well_founded_induction :
+ forall P:A -> Set,
+   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+Theorem well_founded_ind :
+ forall P:A -> Prop,
+   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
@@ -663,25 +715,26 @@ fixpoint equation can be proved.
 \begin{coq_example*}
 Section FixPoint.
 Variable P : A -> Set.
-Variable F : (x:A)((y:A)(R y x)->(P y))->(P x).
-Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) := 
-         (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p))).
-Definition fix := [x:A](Fix_F x (Rwf x)).
-Hypothesis F_ext : 
-  (x:A)(f,g:(y:A)(R y x)->(P y))
-  ((y:A)(p:(R y x))((f y p)=(g y p)))->(F x f)=(F x g).
-Lemma Fix_F_eq
-  : (x:A)(r:(Acc x))
-    (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r).
-Lemma Fix_F_inv : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s).
-Lemma fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)).
+Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
+Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
+  F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
+Definition Fix (x:A) := Fix_F x (Rwf x).
+Hypothesis
+  F_ext :
+    forall (x:A) (f g:forall y:A, R y x -> P y),
+      (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g.
+Lemma Fix_F_eq :
+ forall (x:A) (r:Acc x),
+   F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
+Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
+Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
 \begin{coq_example*}
 End FixPoint.
-End Well_founded. 
+End Well_founded.
 \end{coq_example*}
 
 \subsection{Accessing the {\Type} level}
@@ -705,22 +758,22 @@ The basic library includes the definitions\footnote{This is in module
 \ttindex{notT}
 
 \begin{coq_example*}
-Definition allT := [A:Type][P:A->Prop](x:A)(P x). 
+Definition allT (A: Type) (P:A -> Prop) := forall x:A, P x.
 Section universal_quantification.
-Variable A : Type.
-Variable P : A->Prop.
-Theorem inst :  (x:A)(ALLT x | (P x))->(P x).
-Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(allT ? P).
+Variable A :  Type.
+Variable P : A -> Prop.
+Theorem inst : forall x:A, ( ALL x : _ | P x) -> P x.
+Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> allT _ P.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
 \begin{coq_example*}
 End universal_quantification.
-Inductive  exT [A:Type;P:A->Prop] : Prop
-    := exT_intro : (x:A)(P x)->(exT A P).
-Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
-    := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q).
+Inductive exT (A:Type) (P:A -> Prop) : Prop :=
+    exT_intro : forall x:A, P x -> exT A P.
+Inductive exT2 (A:Type) (P Q:A -> Prop) : Prop :=
+    exT_intro2 : forall x:A, P x -> Q x -> exT2 A P Q.
 \end{coq_example*}
 
 It defines also Leibniz equality \verb:x==y: when \verb:x: and
@@ -735,23 +788,24 @@ It defines also Leibniz equality \verb:x==y: when \verb:x: and
 \ttindex{eqT\_rec\_r}
 
 \begin{coq_example*}
-Inductive eqT [A:Type;x:A] : A -> Prop
-                       := refl_eqT : (eqT A x x).
+Inductive eqT (A:Type) (x:A) : A -> Prop :=
+    refl_eqT : eqT A x x.
 Section Equality_is_a_congruence.
-Variables A,B : Type.
-Variable  f : A->B.
-Variable x,y,z : A.
-Lemma sym_eqT : (x==y) -> (y==x).
-Lemma trans_eqT : (x==y) -> (y==z) -> (x==z).
-Lemma congr_eqT : (x==y)->((f x)==(f y)).
+Variables A B : Type.
+Variable f : A -> B.
+Variables x y z : A.
+Lemma sym_eqT : x = y -> y = x.
+Lemma trans_eqT : x = y -> y = z -> x = z.
+Lemma congr_eqT : x = y -> f x = f y.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
 \begin{coq_example*}
 End Equality_is_a_congruence.
-Hints Immediate sym_eqT sym_not_eqT : core.
-Definition eqT_ind_r: (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)y==x -> (P y).
+Hints Immediate sym_eq sym_not_eqT : core.
+Definition eqT_ind_r :
+  forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -782,12 +836,13 @@ corresponding to the main definitions
 At the end, it defines datatypes at the {\Type} level.
 
 \begin{coq_example*}
-Inductive EmptyT: Type :=.
-Inductive UnitT : Type := IT : UnitT.
-Definition notT := [A:Type] A->EmptyT.
-
-Inductive identityT [A:Type; a:A] : A->Type :=
-     refl_identityT : (identityT A a a).
+Inductive EmptyT : Type :=.
+Inductive UnitT : Type :=
+    IT : UnitT.
+Definition notT (A:Type) := A -> EmptyT.
+Inductive identityT (A:
+                     Type) (a:A) : A -> Type :=
+    refl_identityT : identityT A a a.
 \end{coq_example*}
 
 \section{The standard library}
@@ -899,16 +954,17 @@ Reset Initial.
 \end{coq_eval}
 
 \begin{coq_example*}
-Require Arith.
-Fixpoint even [n:nat] : bool :=
-Cases n of (0) => true 
-        |  (1) => false
-        | (S (S n)) => (even n)
-end.
+Require Import Arith.
+Fixpoint even (n:nat) : bool :=
+  match n with
+  | O => true
+  | S O => false
+  | S (S n) => even n
+  end.
 \end{coq_example*}
 
 \begin{coq_eval}
-Reset Initial. 
+Reset Initial.
 \end{coq_eval}
 
 \subsection{Real numbers library}
@@ -922,8 +978,8 @@ similar to the notation for integer arithmetics (see figure
 This syntax is used parenthesizing by a double back-quote (\verb:``:).
 
 \begin{coq_example}
-Require Reals.
-Check ``2+3``.
+Require Import Reals.
+Check  (2 + 3)%R.
 \end{coq_example}
 
 \subsubsection{Some tactics}
@@ -936,12 +992,12 @@ another real integer constante c2.
 \tacindex{DiscrR}
 
 \begin{coq_example*}
-Require DiscrR.
-Goal ``5<>0``.
+Require Import DiscrR.
+Goal 5%R <> 0%R.
 \end{coq_example*}
 
 \begin{coq_example}
-DiscrR.
+discrR.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -953,12 +1009,12 @@ corresponding conjonctions.
 \tacindex{SplitAbsolu}
 
 \begin{coq_example*}
-Require SplitAbsolu.
-Goal (x:R) ``x <= (Rabsolu x)``.
+Require Import SplitAbsolu.
+Goal forall x:R, (x <= Rabs x)%R.
 \end{coq_example*}
 
 \begin{coq_example}
-Intro;SplitAbsolu.
+intro; split_Rabs.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -971,12 +1027,12 @@ product.
 \tacindex{SplitRmult}
 
 \begin{coq_example*}
-Require SplitRmult.
-Goal (x,y,z:R)``x*y*z<>0``.
+Require Import SplitRmult.
+Goal forall x y z:R, (x * y * z)%R <> 0%R.
 \end{coq_example*}
 
 \begin{coq_example}
-Intros;SplitRmult.
+intros; split_Rmult.
 \end{coq_example}
 
 All this tactics has been written with the new tactic language.\\
@@ -984,7 +1040,7 @@ All this tactics has been written with the new tactic language.\\
 More details are available in this document: {\tt http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\
 
 \begin{coq_eval}
-Reset Initial.  
+Reset Initial.
 \end{coq_eval}
 
 \section{Users' contributions}