Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8

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

17 files changed, 311 insertions, 317 deletions

diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v
index 1e9273f07..1f27fe1ba 100644
--- a/test-suite/modules/Demo.v
+++ b/test-suite/modules/Demo.v
@@ -1,51 +1,51 @@
 Module M.
-  Definition t:=nat.
-  Definition x:=O.
+  Definition t := nat.
+  Definition x := 0.
 End M.
 
 Print M.t.
 
 
 Module Type SIG.
-  Parameter t:Set.
-  Parameter x:t.
+  Parameter t : Set.
+  Parameter x : t.
 End SIG.
 
 
-Module F[X:SIG].
-  Definition t:=X.t->X.t.
-  Definition x:t.
-    Intro.
-    Exact X.x.
+Module F (X: SIG).
+  Definition t := X.t -> X.t.
+  Definition x : t.
+    intro.
+    exact X.x.
   Defined.
-  Definition y:=X.x.
+  Definition y := X.x.
 End F.
 
 
 Module N := F M.
 
 Print N.t.
-Eval Compute in N.t.
+Eval compute in N.t.
 
 
 Module N' : SIG := N.
 
 Print N'.t.
-Eval Compute in N'.t.
+Eval compute in N'.t.
 
 
 Module N'' <: SIG := F N.
 
 Print N''.t.
-Eval Compute in N''.t.
+Eval compute in N''.t.
 
-Eval Compute in N''.x.
+Eval compute in N''.x.
 
 
-Module N''' : SIG with Definition t:=nat->nat  :=  N.
+Module N''' : SIG with Definition t := nat -> nat := N.
 
 Print N'''.t.
-Eval Compute in N'''.t.
+Eval compute in N'''.t.
 
 Print N'''.x.
 
diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index d3e98ae4d..57878a5f1 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -1,19 +1,19 @@
-Definition T:=nat.
+Definition T := nat.
 
-Definition le:=Peano.le.
+Definition le := le.
 
-Hints Unfold le.
+Hint Unfold le.
 
-Lemma le_refl:(n:nat)(le n n).
-  Auto.
+Lemma le_refl : forall n : nat, le n n.
+  auto.
 Qed.
 
-Require Le.
+Require Import Le.
 
-Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
-  EAuto with arith.
+Lemma le_trans : forall n m k : nat, le n m -> le m k -> le n k.
+   eauto with arith.
 Qed.
 
-Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
-  EAuto with arith.
-Qed.
+Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m.
+   eauto with arith.
+Qed.
\ No newline at end of file
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 9ba3fb2e6..354c3957f 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -1,57 +1,57 @@
-Implicit Arguments On.
+Set Implicit Arguments.
+Unset Strict Implicit.
 
-Implicits fst.
-Implicits snd.
+Implicit Arguments fst.
+Implicit Arguments snd.
 
 Module Type PO.
-  Parameter T:Set.
-  Parameter le:T->T->Prop.
+  Parameter T : Set.
+  Parameter le : T -> T -> Prop.
   
-  Axiom le_refl : (x:T)(le x x).
-  Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z).
-  Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y).
+  Axiom le_refl : forall x : T, le x x.
+  Axiom le_trans : forall x y z : T, le x y -> le y z -> le x z.
+  Axiom le_antis : forall x y : T, le x y -> le y x -> x = y.
   
-  Hints Resolve le_refl le_trans le_antis.
+  Hint Resolve le_refl le_trans le_antis.
 End PO.
 
 
-Module Pair[X:PO][Y:PO] <: PO.
-  Definition T:=X.T*Y.T.
-  Definition le:=[p1,p2]
-    (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
+Module Pair (X: PO) (Y: PO) <: PO.
+  Definition T := (X.T * Y.T)%type.
+  Definition le p1 p2 := X.le (fst p1) (fst p2) /\ Y.le (snd p1) (snd p2).
 
-  Hints Unfold le.
+  Hint Unfold le.
 
-  Lemma le_refl : (p:T)(le p p).
-    Info Auto.
+  Lemma le_refl : forall p : T, le p p.
+    info auto.
   Qed.
 
-  Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
-    Unfold le; Intuition; Info EAuto.
+  Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
+    unfold le in |- *;  intuition; info  eauto.
   Qed.    
 
-  Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2).
-    NewDestruct p1.  
-    NewDestruct p2.
-    Unfold le.
-    Intuition.
-    CutRewrite t=t1.
-    CutRewrite t0=t2.
-    Reflexivity.
+  Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
+    destruct p1.  
+    destruct p2.
+    unfold le in |- *.
+     intuition.
+     cutrewrite (t = t1).
+     cutrewrite (t0 = t2).
+    reflexivity.
 
-    Info Auto.
+    info auto.
 
-    Info Auto.
+    info auto.
   Qed.
 
 End Pair.
 
 
 
-Read Module Nat.
+Require Nat.
 
 Module NN := Pair Nat Nat.
 
-Lemma zz_min : (p:NN.T)(NN.le (O,O) p).
-  Info Auto with arith.
-Qed.
+Lemma zz_min : forall p : NN.T, NN.le (0, 0) p.
+  info auto with arith.
+Qed.
\ No newline at end of file
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index 4f4c2066d..014f6c604 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -1,38 +1,40 @@
-Definition ifte := [T:Set][A:Prop][B:Prop][s:(sumbool A B)][th:T][el:T] 
-	   	   if s then [_]th else [_]el.
+Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) 
+  (th el : T) := if s then th else el.
 
-Implicits ifte.
+Implicit Arguments ifte.
 
-Lemma Reflexivity_provable : 
-  (A:Set)(a:A)(s:{a=a}+{~a=a})(EXT x| s==(left ? ? x)).
-Intros.
-Elim s.
-Intro x.
-Split with x; Reflexivity.
+Lemma Reflexivity_provable :
+ forall (A : Set) (a : A) (s : {a = a} + {a <> a}),
+ exists x : _, s = left _ x.
+intros.
+elim s.
+intro x.
+split with x; reflexivity.
 
-Intro.
-Absurd a=a; Auto.
+intro.
+ absurd (a = a); auto.
 
-Save.
+Qed.
 
-Lemma Disequality_provable : 
-  (A:Set)(a,b:A)(~a=b)->(s:{a=b}+{~a=b})(EXT x| s==(right ? ? x)).
-Intros.
-Elim s.
-Intro.
-Absurd a=a; Auto.
+Lemma Disequality_provable :
+ forall (A : Set) (a b : A),
+ a <> b -> forall s : {a = b} + {a <> b}, exists x : _, s = right _ x.
+intros.
+elim s.
+intro.
+ absurd (a = a); auto.
 
-Intro.
-Split with b0; Reflexivity.
+intro.
+split with b0; reflexivity.
 
-Save.
+Qed.
 
 Module Type ELEM.
   Parameter T : Set.
-  Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}.
+  Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}.
 End ELEM.
                                         
-Module Type SET[Elt : ELEM].
+Module Type SET (Elt: ELEM).
   Parameter T : Set.
   Parameter empty : T.
   Parameter add : Elt.T -> T -> T.
@@ -40,56 +42,52 @@ Module Type SET[Elt : ELEM].
 
   (* Axioms *)
 
-  Axiom find_empty_false : 
-      (e:Elt.T) (find e empty) = false.
+  Axiom find_empty_false : forall e : Elt.T, find e empty = false.
 
-  Axiom find_add_true : 
-        (s:T) (e:Elt.T) (find e (add e s)) = true.
+  Axiom find_add_true : forall (s : T) (e : Elt.T), find e (add e s) = true.
 
-  Axiom find_add_false :
-        (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> 
-	(find e (add e' s))=(find e s).
+  Axiom
+    find_add_false :
+      forall (s : T) (e e' : Elt.T), e <> e' -> find e (add e' s) = find e s.
 
 End SET.
 
-Module FuncDict[E : ELEM].
+Module FuncDict (E: ELEM).
   Definition T := E.T -> bool.
-  Definition empty := [e':E.T] false.
-  Definition find := [e':E.T] [s:T] (s e').
-  Definition add := [e:E.T][s:T][e':E.T]
-        (ifte (E.eq_dec e e') true (find e' s)).
+  Definition empty (e' : E.T) := false.
+  Definition find (e' : E.T) (s : T) := s e'.
+  Definition add (e : E.T) (s : T) (e' : E.T) :=
+    ifte (E.eq_dec e e') true (find e' s).
 
-  Lemma find_empty_false : (e:E.T) (find e empty) = false.
-    Auto.
+  Lemma find_empty_false : forall e : E.T, find e empty = false.
+    auto.
   Qed.
 
-  Lemma find_add_true : 
-        (s:T) (e:E.T) (find e (add e s)) = true.
+  Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
 
-    Intros.
-    Unfold find add.
-    Elim (Reflexivity_provable ? ? (E.eq_dec e e)).
-    Intros.
-    Rewrite H.
-    Auto.
+    intros.
+    unfold find, add in |- *.
+    elim (Reflexivity_provable _ _ (E.eq_dec e e)).
+    intros.
+     rewrite H.
+    auto.
 
   Qed.
 
   Lemma find_add_false :
-        (s:T) (e:E.T) (e':E.T) ~(e=e') -> 
-	(find e (add e' s))=(find e s).
-    Intros.
-    Unfold add find.
-    Cut (EXT x:? | (E.eq_dec e' e)==(right ? ? x)).
-    Intros.
-    Elim H0.
-    Intros.
-    Rewrite H1.
-    Unfold ifte.
-    Reflexivity.
-
-    Apply Disequality_provable.
-    Auto.
+   forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
+    intros.
+    unfold add, find in |- *.
+    cut (exists x : _, E.eq_dec e' e = right _ x).
+    intros.
+    elim H0.
+    intros.
+     rewrite H1.
+    unfold ifte in |- *.
+    reflexivity.
+
+    apply Disequality_provable.
+    auto.
 
   Qed.
 
@@ -99,84 +97,81 @@ Module F : SET := FuncDict.
 
 
 Module Nat.
-  Definition T:=nat.
-  Lemma eq_dec :  (a,a':T){a=a'}+{~ a=a'}.
-    Decide Equality.
+  Definition T := nat.
+  Lemma eq_dec : forall a a' : T, {a = a'} + {a <> a'}.
+     decide equality.
   Qed.
 End Nat.
 
 
-Module SetNat:=F Nat. 
+Module SetNat := F Nat. 
 
 
-Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. 
-Apply SetNat.find_empty_false. 
-Save.
+Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. 
+apply SetNat.find_empty_false. 
+Qed.
 
 (***************************************************************************)
-Module Lemmas[G:SET][E:ELEM].
+Module Lemmas (G: SET) (E: ELEM).
 
-  Module ESet:=G E.
+  Module ESet := G E.
 
-  Lemma commute : (S:ESet.T)(a1,a2:E.T) 
-    let S1 = (ESet.add a1 (ESet.add a2 S)) in 
-    let S2 = (ESet.add a2 (ESet.add a1 S)) in
-      (a:E.T)(ESet.find a S1)=(ESet.find a S2). 
+  Lemma commute :
+   forall (S : ESet.T) (a1 a2 : E.T),
+   let S1 := ESet.add a1 (ESet.add a2 S) in
+   let S2 := ESet.add a2 (ESet.add a1 S) in
+   forall a : E.T, ESet.find a S1 = ESet.find a S2. 
   
-    Intros.
-    Unfold S1 S2.
-    Elim (E.eq_dec a a1); Elim (E.eq_dec a a2); Intros H1 H2;
-    Try Rewrite <- H1; Try Rewrite <- H2;
-    Repeat 
-      (Try (Rewrite ESet.find_add_true; Auto);
-       Try (Rewrite ESet.find_add_false; Auto); 
-       Auto).
-  Save.
+    intros.
+    unfold S1, S2 in |- *.
+    elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2;
+     try  rewrite <- H1; try  rewrite <- H2;
+     repeat
+      (try ( rewrite ESet.find_add_true; auto);
+        try ( rewrite ESet.find_add_false; auto); auto).
+  Qed.
 End Lemmas.
 
 
-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.
 
-Module ListDict[E : ELEM]. 
-  Definition T := (list E.T).
+Module ListDict (E: ELEM). 
+  Definition T := list E.T.
   Definition elt := E.T.
    
-  Definition empty := (nil elt).
-  Definition add := [e:elt][s:T] (cons elt e s).
-  Fixpoint find [e:elt; s:T] : bool :=
-        Cases s of 
-          nil => false
-        | (cons e' s') => (ifte (E.eq_dec e e') 
-                                true
-                                (find e s'))
-        end.
-
-  Definition find_empty_false := [e:elt] (refl_equal bool false).
-
-  Lemma find_add_true : 
-        (s:T) (e:E.T) (find e (add e s)) = true.
-    Intros.
-    Simpl.
-    Elim (Reflexivity_provable ? ? (E.eq_dec e e)).
-    Intros.
-    Rewrite H.
-    Auto.
+  Definition empty := nil elt.
+  Definition add (e : elt) (s : T) := cons elt e s.
+  Fixpoint find (e : elt) (s : T) {struct s} : bool :=
+    match s with
+    | nil => false
+    | cons e' s' => ifte (E.eq_dec e e') true (find e s')
+    end.
+
+  Definition find_empty_false (e : elt) := refl_equal false.
+
+  Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
+    intros.
+    simpl in |- *.
+    elim (Reflexivity_provable _ _ (E.eq_dec e e)).
+    intros.
+     rewrite H.
+    auto.
 
   Qed.
   
 
   Lemma find_add_false :
-        (s:T) (e:E.T) (e':E.T) ~(e=e') -> 
-	(find e (add e' s))=(find e s).
-    Intros.
-    Simpl.
-    Elim (Disequality_provable ? ? ? H (E.eq_dec e e')).
-    Intros.
-    Rewrite H0.
-    Simpl.
-    Reflexivity.
-  Save.    
+   forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
+    intros.
+    simpl in |- *.
+    elim (Disequality_provable _ _ _ H (E.eq_dec e e')).
+    intros.
+     rewrite H0.
+    simpl in |- *.
+    reflexivity.
+  Qed.    
   
 
 End ListDict.
@@ -190,4 +185,3 @@ Module L : SET := ListDict.
 
 
 
-
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
index 13c284181..8dadace77 100644
--- a/test-suite/modules/Tescik.v
+++ b/test-suite/modules/Tescik.v
@@ -1,30 +1,30 @@
 
 Module Type ELEM.
-  Parameter A:Set.
-  Parameter x:A.
+  Parameter A : Set.
+  Parameter x : A.
 End ELEM.
 
 Module Nat.
-    Definition A:=nat.
-    Definition x:=O.
+    Definition A := nat.
+    Definition x := 0.
 End Nat. 
 
-Module List[X:ELEM].
-  Inductive list : Set := nil : list 
-		       | cons : X.A -> list -> list.
+Module List (X: ELEM).
+  Inductive list : Set :=
+    | nil : list
+    | cons : X.A -> list -> list.
  
-  Definition head := 
-     [l:list]Cases l of 
-	  nil => X.x 
-	| (cons x _) => x
-     end.
+  Definition head (l : list) := match l with
+                                | nil => X.x
+                                | cons x _ => x
+                                end.
 
-  Definition singl := [x:X.A] (cons x nil).
+  Definition singl (x : X.A) := cons x nil.
   
-  Lemma head_singl : (x:X.A)(head (singl x))=x.
-  Auto.
+  Lemma head_singl : forall x : X.A, head (singl x) = x.
+  auto.
   Qed.
 
 End List.
 
-Module N:=(List Nat).
+Module N := List Nat.
\ No newline at end of file
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
index 0f8eef847..f4dc19b3e 100644
--- a/test-suite/modules/fun_objects.v
+++ b/test-suite/modules/fun_objects.v
@@ -1,32 +1,32 @@
-Implicit Arguments On.
+Set Implicit Arguments.
+Unset Strict Implicit.
 
 Module Type SIG.
-  Parameter id:(A:Set)A->A.
+  Parameter id : forall A : Set, A -> A.
 End SIG.
  
-Module M[X:SIG].
-  Definition idid := (X.id X.id).
-  Definition id := (idid X.id).
+Module M (X: SIG).
+  Definition idid := X.id X.id.
+  Definition id := idid X.id.
 End M.
 
-Module N:=M.
+Module N := M.
 
 Module Nat.
   Definition T := nat.
-  Definition x := O.
-  Definition id := [A:Set][x:A]x.
+  Definition x := 0.
+  Definition id (A : Set) (x : A) := x.
 End Nat.
 
-Module Z:=(N Nat).
+Module Z := N Nat.
 
-Check (Z.idid O).
+Check (Z.idid 0).
 
-Module P[Y:SIG] := N.
+Module P (Y: SIG) := N.
 
-Module Y:=P Nat Z.
-
-Check (Y.id O).
+Module Y := P Nat Z.
 
+Check (Y.id 0).
 
 
 
diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v
index fb734b5d5..9657c685d 100644
--- a/test-suite/modules/grammar.v
+++ b/test-suite/modules/grammar.v
@@ -1,15 +1,15 @@
 Module N.
-Definition f:=plus.
-Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
-Check (f O O).
+Definition f := plus.
+(* <Warning> : Syntax is discontinued *)
+Check (f 0 0).
 End N.
-Check (N.f O O).
+Check (N.f 0 0).
 Import N.
-Check (N.f O O).
-Check (f O O).
-Module M:=N.
-Check (f O O).
-Check (N.f O O).
+Check (f 0 0).
+Check (f 0 0).
+Module M := N.
+Check (f 0 0).
+Check (f 0 0).
 Import M.
-Check (f O O).
-Check (N.f O O).
+Check (f 0 0).
+Check (N.f 0 0).
\ No newline at end of file
diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v
index 94c344bbd..a4f9d3a28 100644
--- a/test-suite/modules/ind.v
+++ b/test-suite/modules/ind.v
@@ -1,13 +1,17 @@
 Module Type SIG.
-  Inductive w:Set:=A:w.
-  Parameter f : w->w.
+  Inductive w : Set :=
+      A : w.
+  Parameter f : w -> w.
 End SIG.
 
-Module M:SIG.
-  Inductive w:Set:=A:w.
-  Definition f:=[x]Cases x of A => A end.
+Module M : SIG.
+  Inductive w : Set :=
+      A : w.
+  Definition f x := match x with
+                    | A => A
+                    end.
 End M.
 
-Module N:=M.
+Module N := M.
 
-Check (N.f M.A).
+Check (N.f M.A).
\ No newline at end of file
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
index a9d22d79d..aad493cee 100644
--- a/test-suite/modules/mod_decl.v
+++ b/test-suite/modules/mod_decl.v
@@ -1,49 +1,49 @@
 Module Type SIG.
-  Axiom A:Set.
+  Axiom A : Set.
 End SIG.
 
 Module M0.
-  Definition A:Set.
-  Exact nat.
-  Save.
+  Definition A : Set.
+  exact nat.
+  Qed.
 End M0.
 
-Module M1:SIG.
-  Definition A:=nat.
+Module M1 : SIG.
+  Definition A := nat.
 End M1.
 
-Module M2<:SIG.
-  Definition A:=nat.
+Module M2 <: SIG.
+  Definition A := nat.
 End M2.
 
-Module M3:=M0.
+Module M3 := M0.
 
-Module M4:SIG:=M0.
+Module M4 : SIG := M0.
 
-Module M5<:SIG:=M0.
+Module M5 <: SIG := M0.
 
 
-Module F[X:SIG]:=X.
+Module F (X: SIG) := X.
 
 
 Module Type T.
 
   Module M0.
-    Axiom A:Set.
+    Axiom A : Set.
   End M0.
   
-  Declare Module M1:SIG.
+  Declare Module M1: SIG.
   
-  Declare Module M2<:SIG.
-    Definition A:=nat.
+  Declare Module M2 <: SIG.
+    Definition A := nat.
   End M2.
   
-  Module M3:=M0.
+  Module M3 := M0.
   
-  Module M4:SIG:=M0.
+  Module M4 : SIG := M0.
   
-  Module M5<:SIG:=M0.
+  Module M5 <: SIG := M0.
 
-  Module M6:=F M0.
+  Module M6 := F M0.
 
 End T.
diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
index 9e74a310d..45cf9f124 100644
--- a/test-suite/modules/modeq.v
+++ b/test-suite/modules/modeq.v
@@ -1,22 +1,22 @@
 Module M.
-  Definition T:=nat.
-  Definition x:T:=O.
+  Definition T := nat.
+  Definition x : T := 0.
 End M.
 
 Module Type SIG.
-  Module M:=Top.M.
+  Module M := Top.M.
   Module Type SIG.
-    Parameter T:Set.
+    Parameter T : Set.
   End SIG.
-  Declare Module N:SIG.
+  Declare Module N: SIG.
 End SIG.
 
 Module Z.
-  Module M:=Top.M.
+  Module M := Top.M.
   Module Type SIG.
-    Parameter T:Set.
+    Parameter T : Set.
   End SIG.
-  Module N:=M.
+  Module N := M.
 End Z.
 
-Module A:SIG:=Z.  
+Module A : SIG := Z.  
\ No newline at end of file
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 58ae2a52d..9d24d6ce4 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -1,18 +1,17 @@
 Module M.
-  Parameter rel:nat -> nat -> Prop.
+  Parameter rel : nat -> nat -> Prop.
 
-  Axiom w : (n:nat)(rel O (S n)).
+  Axiom w : forall n : nat, rel 0 (S n).
 
-  Hints Resolve w.
+  Hint Resolve w.
 
-  Grammar constr constr8 := 
-     not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
+  (* <Warning> : Grammar is replaced by Notation *)
   
   Print Hint *.
 
-  Lemma w1 : (O#(S O)).
-  Auto.
-  Save.
+  Lemma w1 : rel 0 1.
+  auto.
+  Qed.
 
 End M.
 
@@ -24,14 +23,13 @@ Auto.
 
 Import M.
 
-Lemma w1 : (O#(S O)).
-Auto.
-Save.
+Lemma w1 : rel 0 1.
+auto.
+Qed.
 
-Check (O#O).
+Check (rel 0 0).
 Locate rel.
 
 Locate Module M.
 
-Module N:=Top.M.
-
+Module N := Top.M.
diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
index 2231e0849..97337a125 100644
--- a/test-suite/modules/obj.v
+++ b/test-suite/modules/obj.v
@@ -1,16 +1,17 @@
-Implicit Arguments On.
+Set Implicit Arguments.
+Unset Strict Implicit.
 
 Module M. 
-  Definition a:=[s:Set]s.
+  Definition a (s : Set) := s.
   Print a.
 End M.
 
 Print M.a.
 
 Module K.
-  Definition app:=[A,B:Set; f:(A->B); x:A](f x).
+  Definition app (A B : Set) (f : A -> B) (x : A) := f x.
   Module N.
-    Definition apap:=[A,B:Set](app (app 1!A 2!B)).
+    Definition apap (A B : Set) := app (app (A:=A) (B:=B)).
     Print app.
     Print apap.
   End N.
@@ -20,7 +21,6 @@ End K.
 Print K.app.
 Print K.N.apap.
 
-Module W:=K.N.
+Module W := K.N.
 
 Print W.apap.
-
diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v
index 418ece442..070f859ea 100644
--- a/test-suite/modules/objects.v
+++ b/test-suite/modules/objects.v
@@ -1,33 +1,33 @@
 Module Type SET.
-  Axiom T:Set.
-  Axiom x:T.
+  Axiom T : Set.
+  Axiom x : T.
 End SET.
  
-Implicit Arguments On.
+Set Implicit Arguments.
+Unset Strict Implicit.
 
-Module M[X:SET].
+Module M (X: SET).
   Definition T := nat.
-  Definition x := O.
-  Definition f := [A:Set][x:A]X.x.
+  Definition x := 0.
+  Definition f (A : Set) (x : A) := X.x.
 End M.
 
-Module N:=M.
+Module N := M.
 
 Module Nat.
   Definition T := nat.
-  Definition x := O.
+  Definition x := 0.
 End Nat.
 
-Module Z:=(N Nat).
+Module Z := N Nat.
 
-Check (Z.f O).
+Check (Z.f 0).
 
-Module P[Y:SET] := N.
+Module P (Y: SET) := N.
 
-Module Y:=P Z Nat.
-
-Check (Y.f O).
+Module Y := P Z Nat.
 
+Check (Y.f 0).
 
 
 
diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v
index 6061ace34..f806a7c41 100644
--- a/test-suite/modules/pliczek.v
+++ b/test-suite/modules/pliczek.v
@@ -1,3 +1,3 @@
 Require Export plik.
 
-Definition tutu := [X:Set](toto X).
+Definition tutu (X : Set) := toto X.
\ No newline at end of file
diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v
index f1f59df0f..50bfd9604 100644
--- a/test-suite/modules/plik.v
+++ b/test-suite/modules/plik.v
@@ -1,4 +1,3 @@
-Definition toto:=[x:Set]x.
+Definition toto (x : Set) := x.
 
-Grammar constr constr8 := 
-     toto [ "#" constr7($b) ] -> [ (toto $b) ].
+(* <Warning> : Grammar is replaced by Notation *)
\ No newline at end of file
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
index c09a74324..4cb6291df 100644
--- a/test-suite/modules/sig.v
+++ b/test-suite/modules/sig.v
@@ -1,29 +1,29 @@
 Module M.
   Module Type SIG.
-    Parameter T:Set.
-    Parameter x:T.
+    Parameter T : Set.
+    Parameter x : T.
   End SIG.
-  Module N:SIG.
-    Definition T:=nat.
-    Definition x:=O.
+  Module N : SIG.
+    Definition T := nat.
+    Definition x := 0.
   End N.
 End M.
 
-Module N:=M.
+Module N := M.
 
 Module Type SPRYT.
   Module N.
-    Definition T:=M.N.T.
-    Parameter x:T.
+    Definition T := M.N.T.
+    Parameter x : T.
   End N.
 End SPRYT.
 
-Module K:SPRYT:=N.  
-Module K':SPRYT:=M.  
+Module K : SPRYT := N.  
+Module K' : SPRYT := M.  
 
 Module Type SIG.
-  Definition T:Set:=M.N.T.
-  Parameter x:T.
+  Definition T : Set := M.N.T.
+  Parameter x : T.
 End SIG.
 
-Module J:SIG:=M.N.
+Module J : SIG := M.N.
\ No newline at end of file
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
index 1bd4faef0..5eec07758 100644
--- a/test-suite/modules/sub_objects.v
+++ b/test-suite/modules/sub_objects.v
@@ -1,33 +1,32 @@
 Set Implicit Arguments.
+Unset Strict Implicit.
 
 
 Module M.
-  Definition id:=[A:Set][x:A]x.
+  Definition id (A : Set) (x : A) := x.
 
   Module Type SIG.
-    Parameter idid:(A:Set)A->A.
+    Parameter idid : forall A : Set, A -> A.
   End SIG.
 
   Module N.
-    Definition idid:=[A:Set][x:A](id x).
-    Grammar constr constr8 := 
-      not_eq [ "#"  constr7($b) ] -> [ (idid $b) ].
-    Notation inc := (plus (S O)). 
+    Definition idid (A : Set) (x : A) := id x.
+    (* <Warning> : Grammar is replaced by Notation *)
+    Notation inc := (plus 1). 
   End N.
 
-  Definition zero:=(N.idid O).
+  Definition zero := N.idid 0.
 
 End M.
 
-Definition zero := (M.N.idid O).
-Definition jeden := (M.N.inc O).
+Definition zero := M.N.idid 0.
+Definition jeden := M.N.inc 0.
 
-Module Goly:=M.N.
+Module Goly := M.N.
 
-Definition Gole_zero := (Goly.idid O).
-Definition Goly_jeden := (Goly.inc O).
+Definition Gole_zero := Goly.idid 0.
+Definition Goly_jeden := Goly.inc 0.
 
 Module Ubrany : M.SIG := M.N.
 
-Definition Ubrane_zero := (Ubrany.idid O).
-
+Definition Ubrane_zero := Ubrany.idid 0.