passage V8

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

11 files changed, 524 insertions, 381 deletions

diff --git a/doc/.cvsignore b/doc/.cvsignore
index 0f98c0d40..0f2afaa29 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -33,3 +33,4 @@ library.files
 library.files.ls
 library.files.ls.tmp
 library.coqweb.tex
+tradv8
diff --git a/doc/Cases.tex b/doc/Cases.tex
index 109d69581..ad7e6853c 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -81,26 +81,26 @@ maximum of two natural numbers. We can write it in primitive syntax
 by:
 
 \begin{coq_example}
-Fixpoint max [n,m:nat] : nat :=
-   Cases n of
-      O     => m
-   | (S n') => Cases m of
-                  O     => (S n')
-               | (S m') => (S (max n' m'))
-               end
-   end.
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n with
+  | O => m
+  | S n' => match m with
+            | O => S n'
+            | S m' => S (max n' m')
+            end
+  end.
 \end{coq_example}
 
 Using multiple patterns in the definition allows to write:
 
 \begin{coq_example}
 Reset max.
-Fixpoint max [n,m:nat] : nat :=
-   Cases n m of
-      O         _  => m   
-   | (S n') O      => (S n')
-   | (S n') (S m') => (S (max n' m')) 
-   end.
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n, m with
+  | O, _ => m
+  | S n', O => S n'
+  | S n', S m' => S (max n' m')
+  end.
 \end{coq_example}
 
 which will be compiled into the previous form.
@@ -111,7 +111,9 @@ there is at least one constructor in the column of patterns. E.g. the
 following example does not build a \texttt{Cases} expression.
 
 \begin{coq_example}
-Check [x:nat]<nat>Cases x of y => y end.
+Check (fun x:nat => match x return nat with
+                    | y => y
+                    end).
 \end{coq_example}
 
 We can also use ``\texttt{as} patterns'' to associate a name to a
@@ -119,23 +121,23 @@ sub-pattern:
 
 \begin{coq_example}
 Reset max.
-Fixpoint max [n:nat] : nat -> nat :=
-  [m:nat] Cases n m of
-             O     _         => m   
-          | ((S n') as p) O  => p
-          | (S n') (S m')    => (S (max n' m')) 
-         end.
+Fixpoint max (n m:nat) {struct n} : nat :=
+  match n, m with
+  | O, _ => m
+  | S n' as p, O => p
+  | S n', S m' => S (max n' m')
+  end.
 \end{coq_example}
 
 Here is now an example of nested patterns:
 
 \begin{coq_example}
-Fixpoint even [n:nat] : bool :=
-   Cases n of
-      O         => true
-   | (S O)      => false
-   | (S (S n')) => (even n')
-   end.
+Fixpoint even (n:nat) : bool :=
+  match n with
+  | O => true
+  | S O => false
+  | S (S n') => even n'
+  end.
 \end{coq_example}
 
 This is compiled into:
@@ -152,12 +154,12 @@ yields \texttt{true} if the first one is less or equal than the second
 one and \texttt{false} otherwise. We can write it as follows:
 
 \begin{coq_example}
-Fixpoint lef [n,m:nat] : bool :=
-         Cases n m of
-             O     x     => true 
-          |  x     O     => false 
-          | (S n) (S m)  => (lef n m)
-         end.
+Fixpoint lef (n m:nat) {struct m} : bool :=
+  match n, m with
+  | O, x => true
+  | x, O => false
+  | S n, S m => lef n m
+  end.
 \end{coq_example}
 
 Note that the first and the second multiple pattern superpose because
@@ -174,12 +176,12 @@ Another way to write  this function is:
 
 \begin{coq_example}
 Reset lef.
-Fixpoint lef [n,m:nat] : bool :=
-         Cases n m of
-             O     x    => true  
-          | (S n) (S m) => (lef n m)
-          |  _     _    => false
-         end.
+Fixpoint lef (n m:nat) {struct m} : bool :=
+  match n, m with
+  | O, x => true
+  | S n, S m => lef n m
+  | _, _ => false
+  end.
 \end{coq_example}
 
 
@@ -192,12 +194,19 @@ 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.
+Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
-Check [x:nat]Cases x of O => true | (S _) => false | x => true end.
+Check
+  
+  (********** The following is not correct and should produce **********)
+  (**************** Error: This clause is redundant ********************)
+  (* Just to adjust the prompt: *) (fun x:nat =>
+                                      match x with
+                                      | O => true
+                                      | S _ => false
+                                      | x => true
+                                      end).
 \end{coq_example}
 
 \asection{About patterns of parametric types}
@@ -208,33 +217,38 @@ during expansion.
 Consider for example the polymorphic lists:
 
 \begin{coq_example}
-Inductive List [A:Set] :Set := 
-  nil:(List A) 
-| cons:A->(List A)->(List A).
+Inductive List (A:Set) : Set :=
+  | nil : List A
+  | cons : A -> List A -> List A.
 \end{coq_example}
 
 We can check the function {\em tail}:
 
 \begin{coq_example}
-Check [l:(List nat)]Cases l of 
-                             nil        => (nil nat)
-                          | (cons _ l') => l'
-                           end.
+Check
+  (fun l:List nat =>
+     match l with
+     | nil => nil nat
+     | cons _ l' => l'
+     end).
 \end{coq_example}
 
 
 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.
+Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
-Check [l:(List nat)]Cases l of 
-                             (nil A)      => (nil nat)
-                          | (cons A _ l') => l'
-                           end.
+Check
+  
+  (********** The following is not correct and should produce **********)
+  (******** Error: The constructor cons expects 2 arguments ************)
+  (* Just to adjust the prompt: *) (fun l:List nat =>
+                                      match l with
+                                      | nil A => nil nat
+                                      | cons A _ l' => l'
+                                      end).
 \end{coq_example}
 
 
@@ -246,16 +260,16 @@ use the expansion strategy to destructure objects of dependent type.
 Consider the type \texttt{listn} of lists of a certain length:
 
 \begin{coq_example}
-Inductive listn : nat-> Set := 
-  niln : (listn O) 
-| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+Inductive listn : nat -> Set :=
+  | niln : listn 0%N
+  | consn : forall n:nat, nat -> listn n -> listn (S n).
 \end{coq_example}
 
 \asubsection{Understanding dependencies in patterns}
 We can define the function \texttt{length} over \texttt{listn} by:
 
 \begin{coq_example}
-Definition length := [n:nat][l:(listn n)] n.
+Definition length (n:nat) (l:listn n) := n.
 \end{coq_example}
 
 Just for illustrating pattern matching, 
@@ -263,11 +277,11 @@ we can define it by case analysis:
 
 \begin{coq_example}
 Reset length.
-Definition length := [n:nat][l:(listn n)]
-                      Cases l of  
-                         niln         => O 
-                      | (consn n _ _) => (S n) 
-                      end.
+Definition length (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn n _ _ => S n
+  end.
 \end{coq_example}
 
 We can understand the meaning of this definition using the
@@ -281,23 +295,23 @@ Now suppose we split the second pattern  of \texttt{length} into two
 cases so to give an
 alternative definition using nested patterns:
 \begin{coq_example}
-Definition length1:= [n:nat] [l:(listn n)]
-   Cases l of 
-        niln                   => O
-   | (consn n _ niln)          => (S n)
-   | (consn n _ (consn _ _ _)) => (S n)
+Definition length1 (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn n _ niln => S n
+  | consn n _ (consn _ _ _) => S n
   end.
 \end{coq_example}
 
 It is obvious that \texttt{length1} is  another version of
 \texttt{length}. We can also give the following definition:
 \begin{coq_example}
-Definition length2:= [n:nat] [l:(listn n)]
- Cases l of 
-     niln                    => O
- | (consn n _ niln)          => (S O)
- | (consn n _ (consn m _ _)) => (S (S m))
- end.
+Definition length2 (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn n _ niln => 1%N
+  | consn n _ (consn m _ _) => S (S m)
+  end.
 \end{coq_example}
 
 If we forget that \texttt{listn} is a dependent type and we read these
@@ -317,12 +331,12 @@ Thus, the following term \texttt{length3} corresponds to the function
 \texttt{length} but this time defined by case analysis on the dependencies instead of on the list:
 
 \begin{coq_example}
-Definition length3 := [n:nat] [l: (listn n)]
-                         Cases l of 
-                            niln              => O
-                         |  (consn O _ _)     => (S O)
-                         |  (consn (S n) _ _) => (S (S n))
-                         end.
+Definition length3 (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn O _ _ => 1%N
+  | consn (S n) _ _ => S (S n)
+  end.
 \end{coq_example}
 
 When we have nested patterns of dependent types, the semantics of
@@ -358,13 +372,12 @@ is an example where the branches have different type
 and we need to provide the elimination predicate:
 
 \begin{coq_example}
-Fixpoint concat [n:nat; l:(listn n)]
- :  (m:nat) (listn m) -> (listn (plus n m))
- := [m:nat][l':(listn m)] 
-      <[n:nat](listn (plus n m))>Cases l  of 
-         niln          => l'
-      | (consn n' a y) => (consn (plus n' m) a (concat n' y m l'))
-      end.
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+  match l in listn n return listn (n + m) with
+  | niln => l'
+  | consn n' a y => consn (n' + m) a (concat n' y m l')
+  end.
 \end{coq_example}
 
 Recall that a list of patterns is also a pattern. So, when
@@ -377,13 +390,12 @@ been:
 
 \begin{coq_example}
 Reset concat.
-Fixpoint concat [n:nat; l:(listn n)]
-     : (m:nat) (listn m) -> (listn (plus n m)) :=
-  [m:nat][l':(listn m)] 
-    <[n,_:nat](listn (plus n m))>Cases l l' of 
-          niln          x => x
-       | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
-                  end.
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+  match l in listn n, l' return listn (n + m) with
+  | niln, x => x
+  | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+  end.
 \end{coq_example}
 
 Notice that this time, the predicate \texttt{[n,\_:nat](listn (plus n
@@ -401,21 +413,22 @@ 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.
+Set Printing Depth 50.
 \end{coq_eval}
 
 \begin{coq_example}
-Fixpoint concat [n:nat; l:(listn n)] 
-     : (m:nat) (listn m) -> (listn (plus n m)) := 
-  [m:nat][l':(listn m)] 
-   <[n:nat](listn (plus n m))>Cases l l' of 
-        | niln          x => x
-        | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
-        end.
+Fixpoint concat
+ (n:
+  (********** 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: *) nat) (l:listn n) (m:nat)
+ (l':listn m) {struct l} : listn (n + m) :=
+  match l, l' with
+  | niln, x => x
+  | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+  end.
 \end{coq_example}
 
 \asection{Using pattern matching to write proofs}
@@ -430,11 +443,11 @@ the function \texttt{buildlist} that given a natural number
 $n$ builds a list of length $n$ containing zeros as follows:
 
 \begin{coq_example}
-Fixpoint buildlist [n:nat] : (listn n) :=
-    <[n:nat](listn n)>Cases n of 
-           O    => niln 
-       |  (S n) => (consn n O (buildlist n))
-       end.
+Fixpoint buildlist (n:nat) : listn n :=
+  match n return listn n with
+  | O => niln
+  | S n => consn n 0 (buildlist n)
+  end.
 \end{coq_example}
 
 We can also use multiple patterns whenever the elimination predicate has
@@ -444,25 +457,25 @@ Consider the following definition of the predicate less-equal
 \texttt{Le}:
 
 \begin{coq_example}
-Inductive LE : nat->nat->Prop :=
-  LEO: (n:nat)(LE O n)
-| LES: (n,m:nat)(LE n m) -> (LE (S n) (S m)).
+Inductive LE : nat -> nat -> Prop :=
+  | LEO : forall n:nat, LE 0%N n
+  | LES : forall n m:nat, LE n m -> LE (S n) (S m).
 \end{coq_example}
 
 We can use multiple patterns to write  the proof of the lemma
  \texttt{(n,m:nat) (LE n m)}\verb=\/=\texttt{(LE m n)}:
 
 \begin{coq_example}
-Fixpoint dec  [n:nat] : (m:nat)(LE n m) \/ (LE m n) :=
- [m:nat] <[n,m:nat](LE n m) \/ (LE m n)>Cases n m of
-           O   x =>  (or_introl ? (LE x O) (LEO x))
-         | x   O =>  (or_intror (LE x O) ? (LEO x))
-         | ((S n) as n') ((S m) as m') =>
-              Cases (dec n m) of
-                  (or_introl h) => (or_introl ? (LE m' n') (LES n m h))
-               |  (or_intror h) => (or_intror (LE n' m') ? (LES m n h))
-              end
-        end.
+Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n :=
+  match n, m return LE n m \/ LE m n with
+  | O, x => or_introl (LE x 0) (LEO x)
+  | x, O => or_intror (LE x 0) (LEO x)
+  | S n as n', S m as m' =>
+      match dec n m with
+      | or_introl h => or_introl (LE m' n') (LES n m h)
+      | or_intror h => or_intror (LE n' m') (LES m n h)
+      end
+  end.
 \end{coq_example}
 In the example of \texttt{dec} the elimination predicate is binary
 because we destructure two arguments of \texttt{nat} which is a
@@ -494,32 +507,32 @@ Example.
 
 \begin{coq_eval}
 Reset Initial.
-Require Arith.
+Require Import Arith.
 \end{coq_eval}
 
 \begin{coq_example*}
 Inductive list : nat -> Set :=
-| nil : (list O)
-| cons : (n:nat)[m:=(mult (2) n)](list m)->(list (S (S m))).
+  | nil : list 0%N
+  | cons : forall n:nat, let m := (2 * n)%N in list m -> list (S (S m)).
 \end{coq_example*}
 
 In the next example, the local definition is not caught.
 
 \begin{coq_example}
-Fixpoint length [n; l:(list n)] : nat :=
-  Cases l of
-     nil => O
-  | (cons n l0) => (S (length (mult (2) n) l0))
+Fixpoint length n (l:list n) {struct l} : nat :=
+  match l with
+  | nil => 0%N
+  | cons n l0 => S (length (2 * n)%N l0)
   end.
 \end{coq_example}
 
 But in this example, it is.
 
 \begin{coq_example}
-Fixpoint length' [n; l:(list n)] : nat :=
-  Cases l of
-     nil => O
-  | (cons _ m l0) => (S (length' m l0))
+Fixpoint length' n (l:list n) {struct l} : nat :=
+  match l with
+  | nil => 0%N
+  | cons _ m l0 => S (length' m l0)
   end.
 \end{coq_example}
 
@@ -537,10 +550,13 @@ Example:
 
 \begin{coq_example}
 Inductive I : Set :=
-  C1 : nat -> I
-| C2 : I -> I.
+  | C1 : nat -> I
+  | C2 : I -> I.
 Coercion C1 : nat >-> I.
-Check [x]Cases x of (C2 O) => O | _ => O end.
+Check (fun x => match x with
+                | C2 O => 0%N
+                | _ => 0%N
+                end).
 \end{coq_example}
 
 
diff --git a/doc/Coercion.tex b/doc/Coercion.tex
index 69e81f6aa..96fb49272 100644
--- a/doc/Coercion.tex
+++ b/doc/Coercion.tex
@@ -337,11 +337,11 @@ We first give an example of coercion between atomic inductive types
 
 %\begin{\small}
 \begin{coq_example}
-Definition bool_in_nat := [b:bool]if b then O else (S O).
+Definition bool_in_nat (b:bool) := if b then 0%N else 1%N.
 Coercion bool_in_nat : bool >-> nat.
-Check O=true.
+Check (0%N = true).
 Set Printing Coercions.
-Check O=true.
+Check (0%N = true).
 \end{coq_example}
 %\end{small}
 
@@ -357,13 +357,13 @@ We give an example of coercion between classes with parameters.
 
 %\begin{\small}
 \begin{coq_example}
-Parameters C:nat->Set; D:nat->bool->Set; E:bool->Set.
-Parameter f : (n:nat)(C n) -> (D (S n) true).
+Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set).
+Parameter f : forall n:nat, C n -> D (S n) true.
 Coercion f : C >-> D.
-Parameter g : (n:nat)(b:bool)(D n b) -> (E b).
+Parameter g : forall (n:nat) (b:bool), D n b -> E b.
 Coercion g : D >-> E.
-Parameter c : (C O).
-Parameter T : (E true) -> nat.
+Parameter c : C 0.
+Parameter T : E true -> nat.
 Check (T c).
 Set Printing Coercions.
 Check (T c).
@@ -378,10 +378,10 @@ We give now an example using identity coercions.
 
 %\begin{small}
 \begin{coq_example}
-Definition D' := [b:bool](D (S O) b).
+Definition D' (b:bool) := D 1 b.
 Identity Coercion IdD'D : D' >-> D.
 Print IdD'D.
-Parameter d' : (D' true).
+Parameter d' : D' true.
 Check (T d').
 Set Printing Coercions.
 Check (T d').
@@ -400,10 +400,10 @@ is given below:
 
 %\begin{small}
 \begin{coq_example}
-Parameters A,B:Set; h:A->B.
+Parameters (A B : Set) (h : A -> B).
 Coercion h : A >-> B.
-Parameter U : (A -> (E true)) -> nat.
-Parameter t : B -> (C O).
+Parameter U : (A -> E true) -> nat.
+Parameter t : B -> C 0.
 Check (U t).
 Set Printing Coercions.
 Check (U t).
@@ -419,8 +419,8 @@ previous example.
 
 %\begin{small}
 \begin{coq_example}
-Parameter U' : ((C O) -> B) -> nat.
-Parameter t' : (E true) -> A.
+Parameter U' : (C 0 -> B) -> nat.
+Parameter t' : E true -> A.
 Check (U' t').
 Set Printing Coercions.
 Check (U' t').
@@ -444,7 +444,7 @@ Unset Printing Coercions.
 \begin{coq_example}
 Parameter Graph : Type.
 Parameter Node : Graph -> Type.
-Coercion Node : Graph >-> SORTCLASS.
+Coercion Node : Graph >-> Sortclass.
 Parameter G : Graph.
 Parameter Arrows : G -> G -> Type.
 Check Arrows.
@@ -466,12 +466,12 @@ Unset Printing Coercions.
 %\begin{small}
 \begin{coq_example}
 Parameter bij : Set -> Set -> Set.
-Parameter ap : (A,B:Set)(bij A B) -> A -> B.
-Coercion ap : bij >-> FUNCLASS.
-Parameter b : (bij nat nat).
-Check (b O).
+Parameter ap : forall A B:Set, bij A B -> A -> B.
+Coercion ap : bij >-> Funclass.
+Parameter b : bij nat nat.
+Check (b 0%N).
 Set Printing Coercions.
-Check (b O).
+Check (b 0%N).
 \end{coq_example}
 %\end{small}
 
diff --git a/doc/Correctness.tex b/doc/Correctness.tex
index 2e623fa96..a5e378199 100644
--- a/doc/Correctness.tex
+++ b/doc/Correctness.tex
@@ -766,8 +766,8 @@ Here we choose to use the binary integers of \texttt{ZArith}.
 The exponentiation $X^n$ is defined, for $n \ge 0$, in the module 
 \texttt{Zpower}:
 \begin{coq_example*}
-Require ZArith.
-Require Zpower.
+Require Import ZArith.
+Require Import Zpower.
 \end{coq_example*}
 
 In particular, the module \texttt{ZArith} loads a module \texttt{Zmisc}
@@ -780,7 +780,7 @@ derived from the proof \texttt{Zeven\_odd\_dec},
 as explained in section~\ref{prog:booleans}:
 
 \begin{coq_eval}
-Require Ring.
+Require Import Ring.
 \end{coq_eval}
 
 
@@ -789,36 +789,34 @@ Require Ring.
 Then we come to the correctness proof. We first import the \Coq\
 module \texttt{Correctness}:
 \begin{coq_example*}
-Require Correctness.
+Require Import Correctness.
 \end{coq_example*}
 \begin{coq_eval}
-Definition Zsquare := [n:Z](Zmult n n).
-Definition Zdouble := [n:Z]`2*n`.
+Definition Zsquare (n:Z) := n * n.
+Definition Zdouble (n:Z) := 2 * n.
 \end{coq_eval}
 
 Then we introduce all the variables needed by the program:
 \begin{coq_example*}
 Parameter x : Z.
-Global Variable n,m,y : Z ref.
+Global Variable n, m, y :Z ref.
 \end{coq_example*}
 
 At last, we can give the annotated program:
 \begin{coq_example}
 Correctness i_exp
-  { `n >= 0` }
-  begin
-     m := x; y := 1;
-     while !n > 0 do
-       { invariant (Zpower x n@0)=(Zmult y (Zpower m n)) /\ `n >= 0`
-         variant n }
-       (if not (Zeven_odd_bool !n) then y := (Zmult !y !m))
-          { (Zpower x n@0) = (Zmult y (Zpower m (Zdouble (Zdiv2 n)))) };
-       m := (Zsquare !m);
-       n := (Zdiv2 !n)
-     done
-   end
-   { y=(Zpower x n@0) }
-.
+ {n >= 0}
+ begin
+ m := x;
+ y := 1;
+ while (!n>0) do
+   { invariant (Zpower x n@0 = y * Zpower m n /\ n >= 0) variant n }
+ (if (not (Zeven_odd_bool !n)) then y := (Zmult !y !m) else tt)
+ {Zpower x n@0 = y * Zpower m (Zdouble (Zdiv2 n))}; m := (Zsquare !m);
+ n := (Zdiv2 !n)
+ done
+ end
+ {y = Zpower x n@0}.
 \end{coq_example}
 
 The proof obligations require some lemmas involving \texttt{Zpower} and
@@ -865,19 +863,14 @@ Reset n.
 \end{coq_eval}
 \begin{coq_example}
 Correctness r_exp
-  let rec exp (x:Z) (n:Z) : Z { variant n } =
-    { `n >= 0` }
-    (if n = 0 then
-       1
-     else
-       let y = (exp x (Zdiv2 n)) in
-       (if (Zeven_odd_bool n) then
-          (Zmult y y)
-        else
-          (Zmult x (Zmult y y))) { result=(Zpower x n) }
-    ) 
-    { result=(Zpower x n) }
-.
+ let rec exp (x:Z)(n:Z) :Z { variant n } =
+ {n >= 0}
+ (if (n=0) then 1
+ else
+ let y = (exp x (Zdiv2 n)) in
+ (if (Zeven_odd_bool n) then (Zmult y y) else (Zmult x (Zmult y y)))
+ {result = Zpower x n})
+ {result = Zpower x n}.
 \end{coq_example}
 
 You can notice that the specification is simpler in the recursive case:
diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index cdc2d4aaf..c2e3708fd 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -234,9 +234,9 @@ The syntax is the following:
 \Example
 Typical examples are the following:
 \begin{coq_example}
-Extract Inductive unit => unit [ "()" ].
-Extract Inductive bool => bool [ true false ].
-Extract Inductive sumbool => bool [ true false ].
+Extract Inductive unit => "unit" [ "()" ].
+Extract Inductive bool => "bool" [ "true" "false" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
 \end{coq_example}
 
 
@@ -314,7 +314,9 @@ The file {\tt Euclid} contains the proof of Euclidean division
 (theorem {\tt eucl\_dev}). The natural numbers defined in the example
 files are unary integers defined by two constructors $O$ and $S$:
 \begin{coq_example*}
-Inductive nat : Set := O : nat | S : nat -> nat.
+Inductive nat : Set :=
+  | O : nat
+  | S : nat -> nat.
 \end{coq_example*}
 
 This module contains a theorem {\tt eucl\_dev}, and its extracted term
@@ -327,9 +329,9 @@ We can now extract this program to \ocaml:
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Require Euclid.
-Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec. 
-Recursive Extraction eucl_dev.
+Require Import Euclid.
+Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec.
+Recursive Extraction  eucl_dev.
 \end{coq_example}
 
 The inlining of {\tt gt\_wf\_rec} and {\tt lt\_wf\_rec} is not
@@ -379,20 +381,20 @@ treesort}, whose type is shown below:
 
 \begin{coq_eval}
 Reset Initial.
-Require Relation_Definitions. 
-Require PolyList.
-Require Sorting. 
-Require Permutation.
+Require Import Relation_Definitions.
+Require Import PolyList.
+Require Import Sorting.
+Require Import Permutation.
 \end{coq_eval}
 \begin{coq_example}
-Require Heap.
-Check treesort.
+Require Import Heap.
+Check   treesort.
 \end{coq_example}
 
 Let's now extract this function: 
 
 \begin{coq_example}
-Extraction Inline Sorting.sort_rec is_heap_rec.
+Extraction Inline sort_rec is_heap_rec.
 Extraction NoInline list_to_heap.
 Extraction "heapsort" treesort.
 \end{coq_example}
diff --git a/doc/Omega.tex b/doc/Omega.tex
index 2d73a07ba..14bafc2a0 100755
--- a/doc/Omega.tex
+++ b/doc/Omega.tex
@@ -123,14 +123,14 @@ The tactic {\tt Omega}~does not belong to the core system. It should be
 loaded by
 
 \begin{coq_example*}
-Require Omega.
+Require Import Omega.
 \end{coq_example*}
 
 \example{}
 
 \begin{coq_example}
-Goal (m,n:Z) ~ `1+2*m = 2*n`.
-Intros; Omega.
+Goal forall m n:Z, 1 + 2 * m <> 2 * n.
+intros; omega.
 \end{coq_example}
 \begin{coq_eval}
 Abort.
@@ -139,8 +139,8 @@ Abort.
 \example{}
 
 \begin{coq_example}
-Goal (z:Z)`z>0` -> `2*z + 1 > z`.
-Intro; Omega.
+Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
+intro; omega.
 \end{coq_example}
 
 % Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
diff --git a/doc/Polynom.tex b/doc/Polynom.tex
index 2194c3795..d8d16b18a 100644
--- a/doc/Polynom.tex
+++ b/doc/Polynom.tex
@@ -407,17 +407,17 @@ terms generated by rewriting were too big for \Coq's type-checker.
 Let us see why:
 
 \begin{coq_eval}
-Require ZArith.
+Require Import ZArith.
 \end{coq_eval}
 \begin{coq_example}
-Goal (x,y,z:Z)`x + 3 + y + y*z = x + 3 + y + z*y`.
+Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
 \end{coq_example}
 \begin{coq_example*}
-Intros; Rewrite (Zmult_sym y z); Reflexivity. 
+intros; rewrite (Zmult_comm y z); reflexivity.
 Save toto.
 \end{coq_example*}
 \begin{coq_example}
-Print toto.
+Print  toto.
 \end{coq_example}
 
 At each step of rewriting, the whole context is duplicated in the proof
diff --git a/doc/RefMan-cas.tex b/doc/RefMan-cas.tex
index f48242fae..c79c14e9b 100755
--- a/doc/RefMan-cas.tex
+++ b/doc/RefMan-cas.tex
@@ -109,7 +109,10 @@ using the command \texttt{Check}  that displays
 the term with its type :
 
 \begin{coq_example}
-Check [n:nat] Cases n of O => true | _ => false end.
+Check (fun n:nat => match n with
+                    | O => true
+                    | _ => false
+                    end).
 \end{coq_example}
 
 
@@ -128,28 +131,33 @@ Let us illustrate through examples the different aspects of pattern matching.
 Consider for example the function that computes the maximum of two
 natural numbers.  We can write it in primitive syntax by:
 \begin{coq_example}
-Fixpoint max [n,m:nat] : nat :=
-        Case n of
-         (*  O   *) m
-         (* S n' *) [n':nat]Case m of
-                             (* O    *) (S n')
-                             (* S m' *) [m':nat](S (max n' m'))
-                            end
-        end.
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n with
+  | O => 
+      (*  O   *) m
+      (* S n' *) 
+  | S n' =>
+      match m with
+      | O => 
+          (* O    *) S n'
+          (* S m' *) 
+      | S m' => S (max n' m')
+      end
+  end.
 \end{coq_example}
 
 Using patterns in the definitions gives:
 
 \begin{coq_example}
 Reset max.
-Fixpoint max [n,m:nat] : nat :=
-          Cases n of 
-             O     => m
-          | (S n') => Cases m of
-                         O      => (S n')
-                       | (S m') => (S (max n' m'))
-                      end
-         end.
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n with
+  | O => m
+  | S n' => match m with
+            | O => S n'
+            | S m' => S (max n' m')
+            end
+  end.
 \end{coq_example}
 
 Another way to write this definition is to use a multiple pattern to
@@ -157,12 +165,12 @@ Another way to write this definition is to use a multiple pattern to
 
 \begin{coq_example}
 Reset max.
-Fixpoint max [n,m:nat] : nat :=
-          Cases n m of
-             O         _  => m   
-          | (S n') O      => (S n')
-          | (S n') (S m') => (S (max n' m')) 
-         end.
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n, m with
+  | O, _ => m
+  | S n', O => S n'
+  | S n', S m' => S (max n' m')
+  end.
 \end{coq_example}
 
 
@@ -170,7 +178,9 @@ The strategy examines patterns
 from left to right. A case expression is generated {\bf only}  when there is at least one constructor in the column of patterns.
 For example, 
 \begin{coq_example}
-Check [x:nat]<nat>Cases x of y => y end.
+Check (fun x:nat => match x return nat with
+                    | y => y
+                    end).
 \end{coq_example}
 
 
@@ -180,12 +190,12 @@ sub-pattern:
 
 \begin{coq_example}
 Reset max.
-Fixpoint max [n:nat] : nat -> nat :=
-  [m:nat] Cases n m of
-             O     _         => m   
-          | ((S n') as N) O  => N
-          | (S n') (S m')    => (S (max n' m')) 
-         end.
+Fixpoint max (n m:nat) {struct n} : nat :=
+  match n, m with
+  | O, _ => m
+  | S n' as N, O => N
+  | S n', S m' => S (max n' m')
+  end.
 \end{coq_example}
 
 
@@ -197,12 +207,12 @@ yields \verb+true+ if the first one is less or equal than the second
 one and \verb+false+ otherwise. We can write it as follows:
 
 \begin{coq_example}
-Fixpoint lef [n,m:nat] : bool :=
-         Cases n m of
-             O     x     => true 
-          |  x     O     => false 
-          | (S n) (S m)  => (lef n m)
-         end.
+Fixpoint lef (n m:nat) {struct m} : bool :=
+  match n, m with
+  | O, x => true
+  | x, O => false
+  | S n, S m => lef n m
+  end.
 \end{coq_example}
 
 Note that the first and the second  multiple pattern  superpose because the couple of
@@ -219,12 +229,12 @@ Another way to write  this function is:
 
 \begin{coq_example}
 Reset lef.
-Fixpoint lef [n,m:nat] : bool :=
-         Cases n m of
-             O     x    => true  
-          | (S n) (S m) => (lef n m)
-          |  _     _    => false
-         end.
+Fixpoint lef (n m:nat) {struct m} : bool :=
+  match n, m with
+  | O, x => true
+  | S n, S m => lef n m
+  | _, _ => false
+  end.
 \end{coq_example}
 
 
@@ -236,7 +246,12 @@ the second one.
 Terms with useless patterns are accepted by the
 system. For example,
 \begin{coq_example}
-Check [x:nat]Cases x of O => true | (S _) => false | x => true end.
+Check
+  (fun x:nat => match x with
+                | O => true
+                | S _ => false
+                | x => true
+                end).
 \end{coq_example}
 
 is accepted even though the last pattern is never used.
@@ -255,27 +270,31 @@ during expansion.
 Consider for example the polymorphic lists:
 
 \begin{coq_example}
-Inductive List [A:Set] :Set := 
-  nil:(List A) 
-| cons:A->(List A)->(List A).
+Inductive List (A:Set) : Set :=
+  | nil : List A
+  | cons : A -> List A -> List A.
 \end{coq_example}
 
 We can check the function {\em tail}:
 
 \begin{coq_example}
-Check [l:(List nat)]Cases l of 
-                             nil        => (nil nat)
-                          | (cons _ l') => l'
-                           end.
+Check
+  (fun l:List nat =>
+     match l with
+     | nil => nil nat
+     | cons _ l' => l'
+     end).
 \end{coq_example}
 
 
 When we use parameters in patterns there is an error message:
 \begin{coq_example}
-Check [l:(List nat)]Cases l of 
-                             (nil nat)      => (nil nat)
-                          | (cons nat _ l') => l'
-                           end.
+Check
+  (fun l:List nat =>
+     match l with
+     | nil nat => nil nat
+     | cons nat _ l' => l'
+     end).
 \end{coq_example}
 
 
@@ -287,27 +306,27 @@ use the macro to destructure objects of dependent type.
 Consider the type \verb+listn+ of lists of a certain length:
 
 \begin{coq_example}
-Inductive listn : nat-> Set := 
-  niln : (listn O) 
-| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+Inductive listn : nat -> Set :=
+  | niln : listn 0%N
+  | consn : forall n:nat, nat -> listn n -> listn (S n).
 \end{coq_example}
 
 \subsubsection{Understanding dependencies in patterns}
 We can define the function \verb+length+ over \verb+listn+ by :
 
 \begin{coq_example}
-Definition length := [n:nat][l:(listn n)] n.
+Definition length (n:nat) (l:listn n) := n.
 \end{coq_example}
 
 Just for illustrating pattern matching, 
 we can define it by case analysis:
 \begin{coq_example}
 Reset length.
-Definition length := [n:nat][l:(listn n)]
-                      Cases l of  
-                         niln         => O 
-                      | (consn n _ _) => (S n) 
-                      end.
+Definition length (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn n _ _ => S n
+  end.
 \end{coq_example}
 
 We can understand the meaning of this definition using the
@@ -317,23 +336,23 @@ Now suppose we split the second pattern  of \verb+length+ into two
 cases so to give an
 alternative definition using nested patterns:
 \begin{coq_example}
-Definition length1:= [n:nat] [l:(listn n)]
-   Cases l of 
-        niln                   => O
-   | (consn n _ niln)          => (S n)
-   | (consn n _ (consn _ _ _)) => (S n)
+Definition length1 (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn n _ niln => S n
+  | consn n _ (consn _ _ _) => S n
   end.
 \end{coq_example}
 
 It is obvious that \verb+length1+ is  another version of
 \verb+length+. We can also give the following definition:
 \begin{coq_example}
-Definition length2:= [n:nat] [l:(listn n)]
- Cases l of 
-     niln                    => O
- | (consn n _ niln)          => (S O)
- | (consn n _ (consn m _ _)) => (S (S m))
- end.
+Definition length2 (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn n _ niln => 1%N
+  | consn n _ (consn m _ _) => S (S m)
+  end.
 \end{coq_example}
 
 If we forget that \verb+listn+ is a dependent type and we read these
@@ -354,12 +373,12 @@ Thus, the following term \verb+length3+ corresponds to the function
 \verb+length+ but this time defined by case analysis on the dependencies instead of on the list:
 
 \begin{coq_example}
-Definition length3 := [n:nat] [l: (listn n)]
-                         Cases l of 
-                            niln              => O
-                         |  (consn O _ _)     => (S O)
-                         |  (consn (S n) _ _) => (S (S n))
-                         end.
+Definition length3 (n:nat) (l:listn n) :=
+  match l with
+  | niln => 0%N
+  | consn O _ _ => 1%N
+  | consn (S n) _ _ => S (S n)
+  end.
 \end{coq_example}
 
 When we have nested patterns of dependent types, the semantics of
@@ -392,12 +411,12 @@ is an example where the branches have different type
 and we need to provide the elimination predicate:
 
 \begin{coq_example}
-Fixpoint concat [n:nat; l:(listn n)] :(m:nat) (listn m) -> (listn (plus n m))
- := [m:nat][l':(listn m)] 
-       <[n:nat](listn (plus n m))>Cases l  of 
-           niln          => l'
-        | (consn n' a y) => (consn (plus n' m) a (concat n' y m l'))
-        end.
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+  match l in listn n return listn (n + m) with
+  | niln => l'
+  | consn n' a y => consn (n' + m) a (concat n' y m l')
+  end.
 \end{coq_example}
 
 Recall that a list of patterns is also a pattern. So, when
@@ -410,12 +429,12 @@ been:
 
 \begin{coq_example}
 Reset concat.
-Fixpoint concat [n:nat; l:(listn n)] : (m:nat) (listn m) -> (listn (plus n m)) 
-:= [m:nat][l':(listn m)] 
-    <[n,_:nat](listn (plus n m))>Cases l l' of 
-                     niln          x => x
-                  | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
-                  end.
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+  match l in listn n, l' return listn (n + m) with
+  | niln, x => x
+  | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+  end.
 \end{coq_example}
 
 Note that this time, the predicate \verb+[n,_:nat](listn (plus n m))+ is binary because we
@@ -429,12 +448,12 @@ When the arity of the predicate (i.e. number of abstractions) is not
 correct Coq rises an error message. For example:
 
 \begin{coq_example}
-Fixpoint concat [n:nat; l:(listn n)] : (m:nat) (listn m) -> (listn (plus n m)) := 
-[m:nat][l':(listn m)] 
-     <[n:nat](listn (plus n m))>Cases l l' of 
-                     niln          x => x
-                  | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
-                  end.
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+  match l, l' with
+  | niln, x => x
+  | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+  end.
 \end{coq_example}
 
 
@@ -448,11 +467,11 @@ the function \verb+buildlist+ that given a natural number
 $n$ builds a list length $n$ containing zeros as follows:
 
 \begin{coq_example}
-Fixpoint buildlist [n:nat] : (listn n) :=
-    <[n:nat](listn n)>Cases n of 
-           O    => niln 
-       |  (S n) => (consn n O (buildlist n))
-       end.
+Fixpoint buildlist (n:nat) : listn n :=
+  match n return listn n with
+  | O => niln
+  | S n => consn n 0 (buildlist n)
+  end.
 \end{coq_example}
 
 We can also use multiple patterns whenever the elimination predicate has
@@ -462,25 +481,25 @@ Consider the following definition of the predicate less-equal
 \verb+Le+:
 
 \begin{coq_example}
-Inductive Le : nat->nat->Prop :=
-  LeO: (n:nat)(Le O n)
-| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+Inductive Le : nat -> nat -> Prop :=
+  | LeO : forall n:nat, Le 0%N n
+  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
 \end{coq_example}
 
 We can use multiple patterns to write  the proof of the lemma
  \verb+(n,m:nat) (Le n m)\/(Le m n)+:
 
 \begin{coq_example}
-Fixpoint dec  [n:nat] : (m:nat)(Le n m) \/ (Le m n) :=
- [m:nat] <[n,m:nat](Le n m) \/ (Le m n)>Cases n m of
-           O   x =>  (or_introl ? (Le x O) (LeO x))
-         | x   O =>  (or_intror (Le x O) ? (LeO x))
-         | ((S n) as N) ((S m) as M) =>
-              Cases (dec n m) of
-                  (or_introl h) => (or_introl ? (Le M N) (LeS n m h))
-               |  (or_intror h) => (or_intror (Le N M) ? (LeS m n h))
-              end
-        end.
+Fixpoint dec (n m:nat) {struct n} : Le n m \/ Le m n :=
+  match n, m return Le n m \/ Le m n with
+  | O, x => or_introl (Le x 0) (LeO x)
+  | x, O => or_intror (Le x 0) (LeO x)
+  | S n as N, S m as M =>
+      match dec n m with
+      | or_introl h => or_introl (Le M N) (LeS n m h)
+      | or_intror h => or_intror (Le N M) (LeS m n h)
+      end
+  end.
 \end{coq_example}
 In the example of \verb+dec+ the elimination predicate is binary
 because we destructure two arguments of \verb+nat+ that is a
@@ -519,7 +538,9 @@ the constructor \verb+pair+ of cartesian product  with "( , )" in patterns.
 This allows for example, to write the first projection
 of pairs as follows:
 \begin{coq_example}
-Definition fst := [A,B:Set][H:A*B] Cases H of (x,y) => x end.
+Definition fst (A B:Set) (H:A * B) := match H with
+                                      | pair x y => x
+                                      end.
 \end{coq_example}
 The grammar presented in figure \ref{grammar} actually
 contains this extension. 
@@ -615,12 +636,12 @@ Consider the following defintion of a function that yields the last
 element of a list and \verb+O+ if it is empty:
 
 \begin{coq_example}
-Fixpoint last [n:nat; l:(listn n)] : nat :=
-Cases l of
-    (consn _ a niln) => a
- |  (consn m _ x)    => (last m x)
- |   niln            => O
- end.
+Fixpoint last (n:nat) (l:listn n) {struct l} : nat :=
+  match l with
+  | consn _ a niln => a
+  | consn m _ x => last m x
+  | niln => 0%N
+  end.
 \end{coq_example}
 
 It fails because of the priority between patterns, we know that this
@@ -628,12 +649,12 @@ definition is equivalent to the following more explicit one (which
 fails too):
 
 \begin{coq_example*}
-Fixpoint last [n:nat; l:(listn n)] : nat :=
-Cases l of
-    (consn _ a niln)          => a
- |  (consn n _ (consn m b x)) => (last n (consn m b x))
- |   niln                     => O
- end.
+Fixpoint last (n:nat) (l:listn n) {struct l} : nat :=
+  match l with
+  | consn _ a niln => a
+  | consn n _ (consn m b x) => last n (consn m b x)
+  | niln => 0%N
+  end.
 \end{coq_example*}
 
 Note that the recursive call  \sverb{(last n (consn m b x)) } is not
@@ -654,14 +675,14 @@ You can get rid of this problem by writing the definition with \emph{simple
 patterns}:
 
 \begin{coq_example}
-Fixpoint last [n:nat; l:(listn n)] : nat :=
-<[_:nat]nat>Cases l of
-    (consn m a x) => Cases x of
-                         niln => a
-                     |   _    => (last m x)
-                     end
- |   niln         => O
- end.
+Fixpoint last (n:nat) (l:listn n) {struct l} : nat :=
+  match l return nat with
+  | consn m a x => match x with
+                   | niln => a
+                   | _ => last m x
+                   end
+  | niln => 0%N
+  end.
 \end{coq_example}
 
 
diff --git a/doc/RefMan-mod.tex b/doc/RefMan-mod.tex
index 25a0da459..d2648a45d 100644
--- a/doc/RefMan-mod.tex
+++ b/doc/RefMan-mod.tex
@@ -138,11 +138,11 @@ only in module types.
 Let us define a simple module.
 \begin{coq_example}
 Module M.
-  Definition T:=nat.
-  Definition x:=O.
-  Definition y:bool.
-    Exact true.
-  Defined.
+Definition T := nat.
+Definition x := 0%N.
+Definition y : bool.
+  exact true.
+Defined.
 End M.
 \end{coq_example}
 
@@ -157,8 +157,8 @@ Print M.x.
 A simple module type:
 \begin{coq_example}
 Module Type SIG.
-  Parameter T:Set.
-  Parameter x:T.
+Parameter T : Set.
+Parameter x : T.
 End SIG.
 \end{coq_example}
 
@@ -173,7 +173,7 @@ precise specification: the \texttt{y} component is dropped as well
 as the body of \texttt{x}.
 
 \begin{coq_example}
-Module N  :  SIG with Definition T:=nat  :=  M.
+Module N : SIG with Definition T := nat := M.
 Print N.T.
 Print N.x.
 Print N.y.
@@ -189,8 +189,8 @@ one:
 
 \begin{coq_example*}
 Module Type SIG'.
-  Definition T:Set:=nat.
-  Parameter x:T.
+Definition T : Set := nat.
+Parameter x : T.
 End SIG'.
 Module N : SIG' := M.
 \end{coq_example*}
@@ -203,38 +203,38 @@ Print P.y.
 \end{coq_example}
 Now let us create a functor, i.e.\ a parametric module
 \begin{coq_example}
-Module Two[X,Y:SIG].
+Module Two (X Y: SIG).
 \end{coq_example}
 \begin{coq_example*}
-  Definition T:=X.T * Y.T.
-  Definition x:=(X.x, Y.x).
+Definition T := X.T * Y.T.
+Definition x := (X.x, Y.x).
 \end{coq_example*}
 \begin{coq_example}
 End Two.
 \end{coq_example}
 and apply it to our modules and do some computations
 \begin{coq_example}
-Module Q:=Two M N.
-Eval Compute in (plus (Fst Q.x) (Snd Q.x)).
+Module Q := Two M N.
+Eval compute in (fst Q.x + snd Q.x)%N.
 \end{coq_example}
 In the end, let us define a module type with two sub-modules, sharing
 some of the fields and give one of its possible implementations:
 \begin{coq_example}
 Module Type SIG2.
-  Declare Module M1:SIG.
-  Declare Module M2<:SIG.
-    Definition T:=M1.T.
-    Parameter x:T.
-  End M2.
+Declare Module M1 : SIG.
+Declare Module M2 <: SIG.
+Definition T := M1.T.
+Parameter x : T.
+End M2.
 End SIG2.
 \end{coq_example}
 \begin{coq_example*}
 Module Mod <: SIG2.
-  Module M1.
-    Definition T:=nat.
-    Definition x:=(1).
-  End M1.
-  Module M2:=M.
+Module M1.
+Definition T := nat.
+Definition x := 1%N.
+End M1.
+Module M2 := M.
 \end{coq_example*}
 \begin{coq_example}
 End Mod.
diff --git a/doc/tov8 b/doc/tov8
new file mode 100755
index 000000000..b47f482e8
--- /dev/null
+++ b/doc/tov8
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+./tradv8 $1
+mv $1 $1.save
+mv $1.v8 $1
diff --git a/doc/tradv8.ml4 b/doc/tradv8.ml4
new file mode 100644
index 000000000..f050f7537
--- /dev/null
+++ b/doc/tradv8.ml4
@@ -0,0 +1,105 @@
+
+open Printf
+
+let file = Sys.argv.(1)
+
+let cin = open_in file
+let cout = open_out (file ^ ".v8")
+
+let (coq_out, coq_in) as chan = Unix.open_process "coqtop -translate"
+
+let begin_coq = 
+  Str.regexp 
+    "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
+
+let end_coq = 
+  Str.regexp 
+    "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
+
+let new_syntax =
+  Str.regexp "New Syntax:[ \t]*$"
+
+(* on envoie un Check O et on saute les 2 premiers New Syntax *)
+let _ =
+  output_string coq_in "Check O.\n";
+  flush coq_in;
+  while not (Str.string_match new_syntax (input_line coq_out) 0) do () done;
+  while not (Str.string_match new_syntax (input_line coq_out) 0) do () done;
+  printf "** init terminée\n"; flush stdout
+
+let iter_char_until_dot cin f =
+  printf "** entrée dans iter_char\n"; flush stdout;
+  let last_c = ref ' ' in
+  let rec loop () =
+    let c = input_char cin in
+    printf "[%c]" c; flush stdout;
+    f c;
+    if !last_c = '.' && (c = ' ' || c = '\t' || c = '\n') then 
+      () 
+    else begin
+      last_c := c;
+      loop ()
+    end
+  in
+  loop ()
+    
+let trad_commands () =
+  (* on copie toutes les commandes dans un fichier temporaire *)
+  let tmp = Filename.temp_file "trad" ".v" in
+  let tmp_in, end_s = 
+    let tmp_out = open_out tmp in
+    let rec loop () =
+      let s = input_line cin in
+      if Str.string_match end_coq s 0 then begin
+	close_out tmp_out;
+	open_in tmp, s
+      end else begin
+	output_string tmp_out (s ^ "\n");
+	loop ()
+      end
+    in
+    loop ()
+  in
+  ignore (Sys.command (Printf.sprintf "cat %s" tmp));
+  let one_command () =
+    (* on envoie toute la commande a Coq *)
+    iter_char_until_dot tmp_in (fun c -> output_char coq_in c);
+    (* on flush *)
+    flush coq_in;
+    (* on lit la réponse *)
+    try
+      (* 1. on cherche la ligne "New Syntax:" *)
+      while true do 
+	let s = input_line coq_out in
+	if Str.string_match new_syntax s 0 then raise Exit
+      done
+    with Exit ->
+      (* 2. on copie tout jusqu'au point *)
+      printf "** New Syntax trouvé\n"; flush stdout;
+      iter_char_until_dot coq_out (fun c -> output_char cout c);
+      printf "** copie terminée\n"; flush stdout;
+      flush cout
+  in    
+  try
+    while true do one_command () done; assert false
+  with End_of_file ->
+    printf "** End_of_file\n"; flush stdout;
+    Sys.remove tmp;
+    end_s
+
+let trad () =
+  while true do
+    let s = input_line cin in
+    output_string cout (s ^ "\n");
+    if Str.string_match begin_coq s 0 then 
+      let s = trad_commands () in
+      output_string cout (s ^ "\n");
+  done
+
+let _ =
+  try 
+    trad () 
+  with End_of_file -> 
+    close_out cout; 
+    printf "** close_out cout\n"; flush stdout;
+    ignore (Unix.close_process chan)