passage V8

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

3 files changed, 279 insertions, 232 deletions

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 57acfa3c47..a5e8b36622 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -168,16 +168,16 @@ context whose statement's conclusion matches the expression {\term}
 where holes in the latter are denoted by ``{\texttt ?}''.
 
 \begin{coq_example}
-Require Arith.
-SearchPattern (plus ? ?)=?.
+Require Import Arith.
+SearchPattern ((_ + _)%N = _).
 \end{coq_example}
 
 Patterns need not be linear: you can express that the same
 expression must occur in two places by using indexed `{\texttt ?}''.
 
 \begin{coq_example}
-Require Arith.
-SearchPattern (plus ?1 ?)=?1.
+Require Import Arith.
+SearchPattern ((?X1 + _)%N = ?X1).
 \end{coq_example}
 
 \subsection{\tt SearchRewrite {\term}.}\comindex{SearchRewrite}
@@ -187,8 +187,8 @@ context whose statement's conclusion is an equality of which one side matches
 the expression {\term =}. Holes in {\term} are denoted by ``{\texttt ?}''.
 
 \begin{coq_example}
-Require Arith.
-SearchRewrite (plus ? ?).
+Require Import Arith.
+SearchRewrite (_ + _)%N.
 \end{coq_example}
 
 \begin{Variants}
@@ -249,10 +249,11 @@ No module \module{} has been required (see section~\ref{Require}).
 This command displays the full name of the qualified identifier {\qualid}
 and consequently the \Coq\ module in which it is defined.
 
+% (***************** The last line should produce **************************)
+% (************* Error: I.Dont.Exist not a defined object ******************)
+% (* Just to adjust the prompt: *) 
 \begin{coq_eval}
-(***************** The last line should produce **************************)
-(************* Error: I.Dont.Exist not a defined object ******************)
-(* Just to adjust the prompt: *) Set Printing Depth 50.
+Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
 Locate nat.
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 00cd5b134a..cfee66fce2 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -498,12 +498,12 @@ This tactic applies to any goal. It generalizes the conclusion w.r.t. one
 subterm of it. For example:
 
 \begin{coq_eval}
-Goal (x,y:nat) (le O (plus (plus x y) y)).
-Intros.
+Goal forall x y:nat, (0 <= x + y + y)%N.
+intros.
 \end{coq_eval}
 \begin{coq_example}
 Show.
-Generalize (plus (plus x y) y).
+generalize (x + y + y)%N.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -893,9 +893,9 @@ account in the induction hypothesis, then it needs to be removed first
   {\tt Intros until {\ident}; NewInduction {\ident}}.
 
 \begin{coq_example}
-Lemma induction_test : (n:nat) n=n -> (le n n).
-Intros n H.
-NewInduction n.
+Lemma induction_test : forall n:nat, n = n -> (n <= n)%N.
+intros n H.
+induction n.
 \end{coq_example}
 
 \begin{ErrMsgs}
@@ -1052,9 +1052,9 @@ analysis over $X$
 clears $X$ and performs an introduction over the list of patterns $p_1~\ldots~p_n$.
 \end{itemize}
 \begin{coq_example}
-Lemma intros_test : (A,B,C:Prop)(A\/(B/\C))->(A->C)->C.
-Intros A B C [a|(_,c)] f.
-Apply (f a).
+Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
+intros A B C [a| [_ c]] f.
+apply (f a).
 Proof c.
 \end{coq_example}
 
@@ -1083,8 +1083,8 @@ Example:
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Lemma ex1: (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
-Intros A B C H; Decompose [and or] H; Assumption.
+Lemma ex1 : forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
+intros A B C H; decompose [and or] H; assumption.
 \end{coq_example}
 \begin{coq_example*}
 Qed.
@@ -1114,9 +1114,9 @@ and induction following the definition of a function.
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Lemma moins_le : (n,m:nat) (le (minus n m) n).
-Intros n m.
-Functional Induction minus n m;Simpl;Auto.
+Lemma moins_le : forall n m:nat, (n - m <= n)%N.
+intros n m.
+functional induction minus n m; simpl; auto.
 \end{coq_example}
 \begin{coq_example*}
 Qed.
@@ -1373,17 +1373,19 @@ the same positions and puts them as antecedents of the current goal.
 \Example Consider the following goal:
 
 \begin{coq_example*}
-Inductive list : Set  := 
-        nil: list | cons: nat-> list -> list.
-Variable  P : list -> Prop.
+Inductive list : Set :=
+  | nil : list
+  | cons : nat -> list -> list.
+Variable P : list -> Prop.
 \end{coq_example*}
 \begin{coq_eval}
-Lemma ex: (l:list)(n:nat)(P nil)->(cons n l)=(cons O nil)->(P l).
-Intros l n H H0.
+Lemma ex :
+ forall (l:list) (n:nat), P nil -> cons n l = cons 0 nil -> P l.
+intros l n H H0.
 \end{coq_eval}
 \begin{coq_example}
 Show.
-Injection H0.
+injection H0.
 \end{coq_example}
 \begin{coq_eval}
 Abort.
@@ -1652,9 +1654,9 @@ against the hints rather than pattern-matching
 As a consequence, {\tt EAuto} can solve such a goal:
 
 \begin{coq_example}
-Hints Resolve ex_intro.
-Goal (P:nat->Prop)(P O)->(EX n | (P n)).
-EAuto.
+Hints Resolve ex_intro .
+Goal forall P:nat -> Prop, P 0%N ->  EX n : _ | P n.
+eauto.
 \end{coq_example}
 \begin{coq_eval}
 Abort.
@@ -1695,12 +1697,16 @@ The following goal can be proved by {\tt Tauto} whereas {\tt Auto}
 would fail:
 
 \begin{coq_example}
-  Goal (x:nat)(P:nat->Prop)x=O\/(P x)->~x=O->(P x).
-  Intros.
-  Tauto. (* Auto would fail *)
+Goal
+
+  forall (x:nat) (P:nat -> Prop), x = 0%N \/ P x -> x <> 0%N -> P x.
+
+  intros.
+
+  tauto.
 \end{coq_example}
 \begin{coq_eval}
-  Abort.
+Abort.
 \end{coq_eval}
 
 Moreover, if it has nothing else to do, {\tt Tauto} performs
@@ -1708,17 +1714,25 @@ introductions. Therefore, the use of {\tt Intros} in the previous
 proof is unnecessary. {\tt Tauto} can for instance prove the
 following:
 \begin{coq_example}
-  Goal (A:Prop)(P:nat->Prop)(A \/ (x:nat) ~A -> (P x)) -> (x:nat) ~A -> (P x).
-  Tauto.
+Goal
+ (* Auto would fail *)
+  
+  forall (A:Prop) (P:nat -> Prop),
+    A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
+
+  tauto.
 \end{coq_example}
 \begin{coq_eval}
-  Abort.
+Abort.
 \end{coq_eval}
 
 \Rem In contrast, {\tt Tauto} cannot solve the following goal
 
 \begin{coq_example*}
-Goal (A:Prop)(P:nat->Prop)(A \/ (x:nat) ~A -> (P x)) -> (x:nat) ~~ (A \/ (P x)).
+Goal
+
+  forall (A:Prop) (P:nat -> Prop),
+    A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ ~ (A \/ P x).
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -1866,15 +1880,17 @@ normal form.
 
 \Example
 \begin{coq_example*}
-Require ZArithRing.
-Goal (a,b,c:Z)`(a+b+c)*(a+b+c) 
-               = a*a + b*b + c*c + 2*a*b + 2*a*c + 2*b*c`.
+Require Import ZArithRing.
+Goal
+forall a b c:Z,
+  (a + b + c) * (a + b + c) =
+  a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
 \end{coq_example*}
 \begin{coq_example}
-Intros; Ring.
+intros; ring.
 \end{coq_example}
 \begin{coq_eval}
-Reset Initial.  
+Reset Initial.
 \end{coq_eval}
 
 You can have a look at the files \texttt{Ring.v},
@@ -1895,16 +1911,20 @@ the {\tt Add Field} command.
 
 \Example
 \begin{coq_example*}
-Require Reals.
-Goal (x,y:R)``x*y>0`` -> ``x*((1/x)+x/(x+y)) == -(1/y)*y*(-(x*x/(x+y))-1)``.
+Require Import Reals.
+Goal
+  forall x y:R,
+    (x * y > 0)%R ->
+    (x * (1 / x + x / (x + y)))%R =
+    ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.
 \end{coq_example*}
 
 \begin{coq_example}
-Intros; Field.
+intros; field.
 \end{coq_example}
 
 \begin{coq_eval}
-Reset Initial.  
+Reset Initial.
 \end{coq_eval}
 
 \subsection{\tt Add Field}
@@ -1963,17 +1983,17 @@ using Fourier's method (\cite{Fourier}). This tactic must be loaded by
 
 \Example
 \begin{coq_example*}
-Require Reals.
-Require Fourier.
-Goal (x,y:R)``x < y``->``y+1 >= x-1``.
+Require Import Reals.
+Require Import Fourier.
+Goal   forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R.
 \end{coq_example*}
 
 \begin{coq_example}
-Intros; Fourier.
+intros; fourier.
 \end{coq_example}
 
 \begin{coq_eval}
-Reset Initial.  
+Reset Initial.
 \end{coq_eval}
 
 \subsection{\tt AutoRewrite  [ \ident$_1$ \dots \ident$_n$ ]}
@@ -2139,16 +2159,16 @@ Hint discr : core := Extern 4 ~(?=?) Discriminate.
   script. A sub-pattern is a question mark followed by a number like
   \texttt{?1} or \texttt{?2}. Here is an example:
 
+% Require EqDecide.
 \begin{coq_example*}
-Require EqDecide.
-Require PolyList.
+Require Import PolyList.
 \end{coq_example*}
 \begin{coq_example}
-Hint eqdec1 : eqdec := Extern 5 {?1=?2}+{~ (?1=?2)} 
-                                Generalize ?1 ?2; Decide Equality.
-
-Goal (a,b:(list nat*nat)){a=b}+{~a=b}.
-Info Auto with eqdec.
+Hint eqdec1 : eqdec := Extern 5   ({X1 = X2} + {X1 <> X2})
+ generalize X1 X2; decide equality.
+Goal 
+forall a b:list (nat * nat), {a = b} + {a <> b}.
+info auto with eqdec.
 \end{coq_example}
 \begin{coq_eval}
 Abort.
@@ -2477,10 +2497,9 @@ syntax follows the schema:\bigskip
 A simple example has more value than a long explanation: 
 
 \begin{coq_example}
-Tactic Definition Solve := Simpl; Intros; Auto.
-Tactic Definition ElimBoolRewrite b H1 H2 := 
-  Elim b; 
-  [Intros; Rewrite H1; EAuto | Intros; Rewrite H2; EAuto ].
+Ltac Solve := simpl; intros; auto.
+Ltac ElimBoolRewrite b H1 H2 :=
+  elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ].
 \end{coq_example}
 
 The tactics macros are synchronous with the \Coq\ section mechanism:
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 3614aca9af..8fed34e948 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -21,15 +21,19 @@ tactic can be useful to advanced users.
 \Example
 
 \begin{coq_example*}
-Inductive Option: Set := Fail : Option | Ok : bool->Option.
+Inductive Option : Set :=
+  | Fail : Option
+  | Ok : bool -> Option.
 \end{coq_example}
 \begin{coq_example}
-Definition get: (x:Option)~x=Fail->bool.
-Refine
-  [x:Option]<[x:Option]~x=Fail->bool>Cases x of
-        Fail   =>  ?
-      | (Ok b) =>  [_:?]b end.
-Intros;Absurd Fail=Fail;Trivial.
+Definition get : forall x:Option, x <> Fail -> bool.
+refine
+ (fun x:Option =>
+    match x return x <> Fail -> bool with
+    | Fail => _
+    | Ok b => fun _ => b
+    end).
+intros; absurd (Fail = Fail); trivial.
 \end{coq_example}
 \begin{coq_example*}
 Defined.
@@ -104,72 +108,76 @@ Defined.
 Assume we have a relation on {\tt nat} which is transitive:
 
 \begin{coq_example*}
-Variable R:nat->nat->Prop.
-Hypothesis Rtrans : (x,y,z:nat)(R x y)->(R y z)->(R x z).
-Variables n,m,p:nat.
-Hypothesis Rnm:(R n m).
-Hypothesis Rmp:(R m p).
+Variable R : nat -> nat -> Prop.
+Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z.
+Variables n m p : nat.
+Hypothesis Rnm : R n m.
+Hypothesis Rmp : R m p.
 \end{coq_example*}
 
 Consider the goal {\tt (R n p)} provable using the transitivity of
 {\tt R}:
 
 \begin{coq_example*}
-Goal (R n p).
+Goal R n p.
 \end{coq_example*}
 
 The direct application of {\tt Rtrans} with {\tt Apply} fails because
 no value for {\tt y} in {\tt Rtrans} is found by {\tt Apply}:
 
 \begin{coq_eval}
-(********** The following is not correct and should produce **********)
-(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
-(* Just to adjust the prompt: *) Set Printing Depth 50.
+Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
-Apply Rtrans.
+
+(********** The following is not correct and should produce **********)
+(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
+(* Just to adjust the prompt: *) apply Rtrans.
 \end{coq_example}
 
 A solution is to rather apply {\tt (Rtrans n m p)}.
 
 \begin{coq_example}
-Apply (Rtrans n m p).
+apply (Rtrans n m p).
 \end{coq_example}
 
 \begin{coq_eval}
-  Undo.
+Undo.
 \end{coq_eval}
 
 More elegantly, {\tt Apply Rtrans with y:=m} allows to only mention
 the unknown {\tt m}:
 
 \begin{coq_example}
-Apply Rtrans with y:=m.
+
+  apply Rtrans with (y := m).
 \end{coq_example}
 
 \begin{coq_eval}
-  Undo.
+Undo.
 \end{coq_eval}
 
 Another solution is to mention the proof of {\tt (R x y)} in {\tt
 Rtrans}...
 
 \begin{coq_example}
-Apply Rtrans with 1:=Rnm.
+
+  apply Rtrans with (1 := Rnm).
 \end{coq_example}
 
 \begin{coq_eval}
-  Undo.
+Undo.
 \end{coq_eval}
 
 ... or the proof of {\tt (R y z)}:
 
 \begin{coq_example}
-Apply Rtrans with 2:=Rmp.
+
+  apply Rtrans with (2 := Rmp).
 \end{coq_example}
 
 \begin{coq_eval}
-  Undo.
+Undo.
 \end{coq_eval}
 
 On the opposite, one can use {\tt EApply} which postpone the problem
@@ -177,13 +185,14 @@ of finding {\tt m}. Then one can apply the hypotheses {\tt Rnm} and {\tt
 Rmp}. This instantiates the existential variable and completes the proof.
 
 \begin{coq_example}
-EApply Rtrans.
-Apply Rnm.
-Apply Rmp.
+
+  eapply Rtrans.
+apply Rnm.
+apply Rmp.
 \end{coq_example}
 
 \begin{coq_eval}
-  Reset R.
+Reset R.
 \end{coq_eval}
 
 \section{{\tt Scheme}}
@@ -198,15 +207,19 @@ The definition of principle of mutual induction for {\tt tree} and
 
 \begin{coq_eval}
 Reset Initial.
-Variables A,B:Set.
-Mutual 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*}
-Scheme tree_forest_rec := Induction for tree Sort Set 
-with forest_tree_rec := Induction for forest Sort Set.
+Scheme tree_forest_rec := Induction for tree
+  Sort Set
+  with forest_tree_rec := Induction for forest Sort Set.
 \end{coq_example*}
 
 You may now look at the type of {\tt tree\_forest\_rec}:
@@ -235,19 +248,19 @@ Reset Initial.
 \end{coq_eval}
 
 \begin{coq_example*}
-Mutual Inductive odd : nat->Prop := 
-    oddS : (n:nat)(even n)->(odd (S n))
-with even : nat -> Prop := 
-    evenO : (even O) 
-  | evenS : (n:nat)(odd n)->(even (S n)).  
+Inductive odd : nat -> Prop :=
+    oddS : forall n:nat, even n -> odd (S n)
+with even : nat -> Prop :=
+  | evenO : even 0%N
+  | evenS : forall n:nat, odd n -> even (S n).
 \end{coq_example*}
 
 The following command generates a powerful elimination
 principle:
 
 \begin{coq_example*}
-Scheme odd_even := Minimality for odd Sort Prop
-with   even_odd := Minimality for even Sort Prop.
+Scheme odd_even := Minimality for   odd Sort Prop
+  with even_odd := Minimality for even Sort Prop.
 \end{coq_example*}
 
 The type of {\tt odd\_even} for instance will be:
@@ -259,7 +272,7 @@ Check odd_even.
 The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
-\section{{\tt Functional Scheme and Functional Induction}}
+\section{{\tt Functional Scheme} and {\tt Functional Induction}}
 \comindex{FunScheme}
 \label{FunScheme-examples}
 
@@ -273,15 +286,15 @@ Reset Initial.
 \end{coq_eval}
 
 \begin{coq_example*}
-Require Arith.
-Fixpoint div2 [n:nat] : nat :=
- Cases n of
-   (0) => (0)
-   | (S n0) => Cases n0 of
-                    (0) => (0)
-                  | (S n') => (S (div2 n'))
-                 end
- end.
+Require Import Arith.
+Fixpoint div2 (n:nat) : nat :=
+  match n with
+  | O => 0%N
+  | S n0 => match n0 with
+            | O => 0%N
+            | S n' => S (div2 n')
+            end
+  end.
 \end{coq_example*}
 
 The definition of a principle of induction corresponding to the
@@ -301,20 +314,21 @@ We can now prove the following lemma using this principle:
 
 
 \begin{coq_example*}
-Lemma div2_le' : (n:nat)(le (div2 n) n).
-Intro n. Pattern n.
+Lemma div2_le' : forall n:nat, (div2 n <= n)%N.
+intro n.
+ pattern n.
 \end{coq_example*}
 
 
 \begin{coq_example}
-Apply div2_ind;Intros.
+apply div2_ind; intros.
 \end{coq_example}
 
 \begin{coq_example*}
-Auto with arith.
-Auto with arith.
-Simpl;Auto with arith.
-Save.
+auto with arith.
+auto with arith.
+simpl; auto with arith.
+Qed.
 \end{coq_example*}
 
 Since \texttt{div2} is not mutually recursive, we can use
@@ -323,19 +337,19 @@ building the principle:
 
 \begin{coq_example*}
 Reset div2_ind.
-Lemma div2_le : (n:nat)(le (div2 n) n).
-Intro n.
+Lemma div2_le : forall n:nat, (div2 n <= n)%N.
+intro n.
 \end{coq_example*}
 
 \begin{coq_example}
-Functional Induction div2 n.
+functional induction div2 n.
 \end{coq_example}
 
 \begin{coq_example*}
-Auto with arith.
-Auto with arith.
-Auto with arith.
-Save.
+auto with arith.
+auto with arith.
+auto with arith.
+Qed.
 \end{coq_example*}
 
 \paragraph{remark:} \texttt{Functional Induction} makes no use of
@@ -358,23 +372,26 @@ We define trees by the following mutual inductive type:
 
 \begin{coq_example*}
 Variable A : Set.
-Mutual Inductive 
-     tree   : Set := node : A -> forest -> tree
-with forest : Set := empty : forest 
-                  | cons : tree -> forest -> forest.
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | empty : forest
+  | cons : tree -> forest -> forest.
 \end{coq_example*}
 
 We define the function \texttt{tree\_size} that computes the size
 of a tree or a forest.
 
 \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
-  empty => 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
+  | empty => 0%N
+  | cons t f' => (tree_size t + forest_size f')%N
+  end.
 \end{coq_example*}
 
 The definition of principle of mutual induction following the
@@ -382,7 +399,8 @@ recursive structure of \texttt{tree\_size} is defined by the
 command:
 
 \begin{coq_example*}
-Functional Scheme treeInd := Induction for tree_size with tree_size forest_size.
+Functional Scheme treeInd := Induction for tree_size
+ with tree_size forest_size.
 \end{coq_example*}
 
 You may now look at the type of {\tt treeInd}:
@@ -441,17 +459,18 @@ Reset Initial.
 \end{coq_eval}
 
 \begin{coq_example*}
-Inductive Le : nat->nat->Set :=
-  LeO : (n:nat)(Le O n)  |  LeS : (n,m:nat) (Le n m)-> (Le (S n) (S m)).
-Variable P:nat->nat->Prop.
-Variable Q:(n,m:nat)(Le n m)->Prop.
+Inductive Le : nat -> nat -> Set :=
+  | LeO : forall n:nat, Le 0%N n
+  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
+Variable P : nat -> nat -> Prop.
+Variable Q : forall n m:nat, Le n m -> Prop.
 \end{coq_example*}
 
 For example, consider the goal:
 
 \begin{coq_eval}
-Lemma ex : (n,m:nat)(Le (S n) m)->(P n m).
-Intros.
+Lemma ex : forall n m:nat, Le (S n) m -> P n m.
+intros.
 \end{coq_eval}
 
 \begin{coq_example}
@@ -469,7 +488,7 @@ This inversion is possible because \texttt{Le} is the smallest set closed by
 the constructors \texttt{LeO} and \texttt{LeS}.
 
 \begin{coq_example}
-Inversion_clear  H.
+inversion_clear H.
 \end{coq_example}
 
 Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)}
@@ -486,7 +505,7 @@ Undo.
 \end{coq_example*}
 
 \begin{coq_example}
-Inversion H.
+inversion H.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -498,8 +517,8 @@ Undo.
 Let us consider the following goal:
 
 \begin{coq_eval}
-Lemma ex_dep : (n,m:nat)(H:(Le (S n) m))(Q (S n) m H).
-Intros.
+Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H.
+intros.
 \end{coq_eval}
 
 \begin{coq_example}
@@ -514,7 +533,7 @@ substitution.
 To have such a behavior we use the dependent inversion tactics:
 
 \begin{coq_example}
-Dependent Inversion_clear H.
+dependent inversion_clear H.
 \end{coq_example}
 
 Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
@@ -530,7 +549,8 @@ For example, to generate the inversion lemma for the instance
 \texttt{(Le (S n) m)} and the sort \texttt{Prop} we do:
 
 \begin{coq_example*}
-Derive Inversion_clear leminv with (n,m:nat)(Le (S n) m) Sort Prop.
+Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort
+ Prop.
 \end{coq_example*}
 
 \begin{coq_example}
@@ -544,7 +564,7 @@ Show.
 \end{coq_example}
 
 \begin{coq_example}
-Inversion H using leminv.
+inversion H using leminv.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -565,46 +585,50 @@ rewritings and shows how to deal with them using the optional tactic of the
 %Here is a basic use of {\tt AutoRewrite} with the Ackermann function:
 
 \begin{coq_example*}
-Require Arith.
-
-Variable Ack:nat->nat->nat.
-
-Axiom Ack0:(m:nat)(Ack (0) m)=(S m).
-Axiom Ack1:(n:nat)(Ack (S n) (0))=(Ack n (1)).
-Axiom Ack2:(n,m:nat)(Ack (S n) (S m))=(Ack n (Ack (S n) m)).
+Require Import Arith.
+Variable Ack : 
+           nat -> nat -> nat.
+Axiom Ack0 : 
+        forall m:nat, Ack 0 m = S m.
+Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
+Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
 \end{coq_example*}
 
 \begin{coq_example}
 Hint Rewrite [ Ack0 Ack1 Ack2 ] in base0.
-
-Lemma ResAck0:(Ack (3) (2))=(29).
-AutoRewrite [ base0 ] using Try Reflexivity.
+Lemma ResAck0 : 
+ Ack 3 2 = 29%N.
+autorewrite [ base0 ] using try reflexivity.
 \end{coq_example}
 
 \begin{coq_eval}
-Reset Initial.  
+Reset Initial.
 \end{coq_eval}
 
 \example{Mac Carthy function}
 %The Mac Carthy function shows a more complex case:
 
 \begin{coq_example*}
-Require Omega.
-
-Variable g:nat->nat->nat.
-
-Axiom g0:(m:nat)(g (0) m)=m.
-Axiom g1:
-  (n,m:nat)(gt n (0))->(gt m (100))->(g n m)=(g (pred n) (minus m (10))).
-Axiom g2:
-  (n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))).
+Require Import Omega.
+Variable g :   
+           nat -> nat -> nat.
+Axiom g0 : 
+        forall m:nat, g 0 m = m.
+Axiom
+  g1 :
+    forall n m:nat,
+      (n > 0)%N -> (m > 100)%N -> g n m = g (pred n) (m - 10).
+Axiom
+  g2 :
+    forall n m:nat,
+      (n > 0)%N -> (m <= 100)%N -> g n m = g (S n) (m + 11).
 \end{coq_example*}
 
 \begin{coq_example}
-Hint Rewrite [ g0 g1 g2 ] in base1 using Omega.
-
-Lemma Resg0:(g (1) (110))=(100).
-AutoRewrite [ base1 ] using Reflexivity Orelse Simpl.
+Hint Rewrite [ g0 g1 g2 ] in base1 using omega.
+Lemma Resg0 : 
+ g 1 110 = 100%N.
+autorewrite [ base1 ] using reflexivity || simpl.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -612,8 +636,8 @@ Abort.
 \end{coq_eval}
 
 \begin{coq_example}
-Lemma Resg1:(g (1) (95))=(91).
-AutoRewrite [ base1 ] using Reflexivity Orelse Simpl.
+Lemma Resg1 : g 1 95 = 91%N.
+autorewrite [ base1 ] using reflexivity || simpl.
 \end{coq_example}
 
 \begin{coq_eval}
@@ -637,25 +661,25 @@ will replace the head of current goal by a convertible term of the form
 Here is an example:
 
 \begin{coq_example}
-Require Quote.
-Parameters A,B,C:Prop.
-Inductive Type formula :=
-| f_and : formula -> formula -> formula (* binary constructor *)
-| f_or : formula -> formula -> formula  
-| f_not : formula -> formula            (* unary constructor *)
-| f_true : formula                      (* 0-ary constructor *)
-| f_const : Prop -> formula             (* contructor for constants *).
-
-Fixpoint interp_f [f:formula] : Prop := 
-  Cases f of
-  | (f_and f1 f2) => (interp_f f1)/\(interp_f f2)
-  | (f_or f1 f2) => (interp_f f1)\/(interp_f f2)
-  | (f_not f1) => ~(interp_f f1)
+Require Import Quote.
+Parameters A B C : Prop.
+Inductive formula : Type :=
+  | f_and : formula -> formula -> formula (* binary constructor *)
+  | f_or : formula -> formula -> formula
+  | f_not : formula -> formula (* unary constructor *)
+  | f_true : formula (* 0-ary constructor *)
+  | f_const : Prop -> formula (* contructor for constants *).
+Fixpoint interp_f (f:
+                   formula) : Prop :=
+  match f with
+  | f_and f1 f2 => interp_f f1 /\ interp_f f2
+  | f_or f1 f2 => interp_f f1 \/ interp_f f2
+  | f_not f1 => ~ interp_f f1
   | f_true => True
-  | (f_const c) => c
+  | f_const c => c
   end.
-Goal A/\(A\/True)/\~B/\(A <-> A).
-Quote interp_f.
+Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A).
+quote interp_f.
 \end{coq_example}
 
 The algorithm to perform this inversion is: try to match the
@@ -696,12 +720,12 @@ It is better to use that type of formulas:
 Reset formula.
 \end{coq_eval}
 \begin{coq_example}
-Inductive Set formula :=
-| f_and : formula -> formula -> formula
-| f_or : formula -> formula -> formula  
-| f_not : formula -> formula           
-| f_true : formula                     
-| f_atom : index -> formula.
+Inductive formula : Set :=
+  | f_and : formula -> formula -> formula
+  | f_or : formula -> formula -> formula
+  | f_not : formula -> formula
+  | f_true : formula
+  | f_atom : index -> formula.
 \end{coq_example*}
 
 \texttt{index} is defined in module \texttt{Quote}. Equality on that
@@ -715,21 +739,22 @@ provides also a type \texttt{(varmap A)} of bindings from
 function has now another argument, a variables map:
 
 \begin{coq_example}
- Fixpoint interp_f [vm:(varmap Prop); f:formula] : Prop := 
-  Cases f of
-  | (f_and f1 f2) => (interp_f vm f1)/\(interp_f vm f2)
-  | (f_or f1 f2) => (interp_f vm f1)\/(interp_f vm f2)
-  | (f_not f1) => ~(interp_f vm f1)
+Fixpoint interp_f (vm:
+                    varmap Prop) (f:formula) {struct f} : Prop :=
+  match f with
+  | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
+  | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
+  | f_not f1 => ~ interp_f vm f1
   | f_true => True
-  | (f_atom i) => (varmap_find True i vm)
+  | f_atom i => varmap_find True i vm
   end.
 \end{coq_example}
 
 \noindent\texttt{Quote} handles this second case properly:
 
 \begin{coq_example}
-Goal A/\(B\/A)/\(A\/~B).
-Quote interp_f.
+Goal A /\ (B \/ A) /\ (A \/ ~ B).
+quote interp_f.
 \end{coq_example}
 
 It builds \texttt{vm} and \texttt{t} such that \texttt{(f vm t)} is
@@ -750,30 +775,32 @@ Example:
 Reset formula.
 \end{coq_eval}
 \begin{coq_example*}
-Inductive Type formula :=
-| f_and : formula -> formula -> formula
-| f_or : formula -> formula -> formula
-| f_not : formula -> formula
-| f_true : formula
-| f_const : Prop -> formula             (* constructor for constants *)
-| f_atom : index -> formula.            (* constructor for variables *)
-
-Fixpoint interp_f [vm:(varmap Prop); f:formula] : Prop := 
-  Cases f of
-  | (f_and f1 f2) => (interp_f vm f1)/\(interp_f vm f2)
-  | (f_or f1 f2) => (interp_f vm f1)\/(interp_f vm f2)
-  | (f_not f1) => ~(interp_f vm f1)
+Inductive formula : Type :=
+  | f_and : formula -> formula -> formula
+  | f_or : formula -> formula -> formula
+  | f_not : formula -> formula
+  | f_true : formula
+  | f_const : Prop -> formula (* constructor for constants *)
+  | f_atom : index -> formula.
+Fixpoint interp_f
+ (vm:            (* constructor for variables *)
+  varmap Prop) (f:formula) {struct f} : Prop :=
+  match f with
+  | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
+  | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
+  | f_not f1 => ~ interp_f vm f1
   | f_true => True
-  | (f_const c) => c
-  | (f_atom i) => (varmap_find True i vm)
+  | f_const c => c
+  | f_atom i => varmap_find True i vm
   end.
-
-Goal A/\(A\/True)/\~B/\(C<->C).
+Goal 
+A /\ (A \/ True) /\ ~ B /\ (C <-> C).
 \end{coq_example*}
 
 \begin{coq_example}
-Quote interp_f [A B]. 
-Undo. Quote interp_f [B C iff]. 
+quote interp_f [ A B ].
+Undo.
+  quote interp_f [ B C iff ].
 \end{coq_example}
 
 \Warning Since function inversion