Petites corrections ici et la

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

9 files changed, 129 insertions, 106 deletions

diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v
index 9d8c49ef7..9773bc6f4 100644
--- a/test-suite/modules/Nametab.v
+++ b/test-suite/modules/Nametab.v
@@ -1,35 +1,35 @@
-Module M.
-  Definition id:=[x:Set]x.
-  Module M.
-    Definition zero:(id nat):= O.
-    Definition id:=Set.
-    Definition nacik:id:=nat.
-  End M.
-End M.
-
-Module M.
+Module Q.
 Module N.
 Module K.
 Definition id:=Set.
 End K.
 End N.
-End M.
-
+End Q.
 
 Locate id.
 Locate K.id.
 Locate N.K.id.
-Locate M.N.K.id.
-Locate Top.M.N.K.id.
+Locate Q.N.K.id.
+Locate Top.Q.N.K.id.
 Locate K.
 Locate N.K.
-Locate M.N.K.
-Locate Scratch.M.N.K.
+Locate Q.N.K.
+Locate Top.Q.N.K.
 Locate N.
-Locate M.N.
-Locate Scratch.M.N.
-Locate M.
-Locate Scratch.M.
+Locate Q.N.
+Locate Top.Q.N.
+Locate Q.
+Locate Top.Q.
+
+
+Module Type SIG.
+End SIG.
+
+Module Type FSIG[X:SIG].
+End FSIG.
+
+Module F[X:SIG].
+End F.
 
 (*
 #trace Nametab.push;;
@@ -40,46 +40,74 @@ Locate Scratch.M.
 *)
 
 Module M.
+Reset M.
 Module M[X:SIG].
+Reset M.
 Module M[X,Y:SIG].
+Reset M.
 Module M[X:SIG;Y:SIG].
-Module M[X,Y:SIG;X,Z:SIG].
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG].
+Reset M.
 Module M[X:SIG][Y:SIG].
-Module M[X,Y:SIG][X,Z:SIG].
+Reset M.
+Module M[X,Y:SIG][Z1,Z:SIG].
+Reset M.
 Module M:SIG.
+Reset M.
 Module M[X:SIG]:SIG.
+Reset M.
 Module M[X,Y:SIG]:SIG.
+Reset M.
 Module M[X:SIG;Y:SIG]:SIG.
-Module M[X,Y:SIG;X,Z:SIG]:SIG.
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG]:SIG.
+Reset M.
 Module M[X:SIG][Y:SIG]:SIG.
-Module M[X,Y:SIG][X,Z:SIG]:SIG.
-Module M:=(M N).
-Module M[X:SIG]:=(M N).
-Module M[X,Y:SIG]:=(M N).
-Module M[X:SIG;Y:SIG]:=(M N).
-Module M[X,Y:SIG;X,Z:SIG]:=(M N).
-Module M[X:SIG][Y:SIG]:=(M N).
-Module M[X,Y:SIG][X,Z:SIG]:=(M N).
-Module M:SIG:=(M N).
-Module M[X:SIG]:SIG:=(M N).
-Module M[X,Y:SIG]:SIG:=(M N).
-Module M[X:SIG;Y:SIG]:SIG:=(M N).
-Module M[X,Y:SIG;X,Z:SIG]:SIG:=(M N).
-Module M[X:SIG][Y:SIG]:SIG:=(M N).
-Module M[X,Y:SIG][X,Z:SIG]:SIG:=(M N).
+Reset M.
+Module M[X,Y:SIG][Z1,Z:SIG]:SIG.
+Reset M.
+Module M:=(F Q).
+Reset M.
+Module M[X:FSIG]:=(X Q).
+Reset M.
+Module M[X,Y:FSIG]:=(X Q).
+Reset M.
+Module M[X:FSIG;Y:SIG]:=(X Y).
+Reset M.
+Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z).
+Reset M.
+Module M[X:FSIG][Y:SIG]:=(X Y).
+Reset M.
+Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z).
+Reset M.
+Module M:SIG:=(F Q).
+Reset M.
+Module M[X:FSIG]:SIG:=(X Q).
+Reset M.
+Module M[X,Y:FSIG]:SIG:=(X Q).
+Reset M.
+Module M[X:FSIG;Y:SIG]:SIG:=(X Y).
+Reset M.
+Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z).
+Reset M.
+Module M[X:FSIG][Y:SIG]:SIG:=(X Y).
+Reset M.
+Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z).
+Reset M.
 
 
-Moduletype SIG.
+Module Type ELEM.
   Parameter A:Set.
   Parameter x:A.
-EndT SIG.
+End ELEM.
 
 Module Nat.
     Definition A:=nat.
     Definition x:=O.
 End Nat. 
 
-Module List[X:SIG].
+Module List[X:ELEM].
   Inductive list : Set := nil : list 
 		       | cons : X.A -> list -> list.
  
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index ecf9a8c25..4f4c2066d 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -27,12 +27,12 @@ Split with b0; Reflexivity.
 
 Save.
 
-Modtype ELEM.
+Module Type ELEM.
   Parameter T : Set.
   Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}.
-EndT ELEM.
+End ELEM.
                                         
-Modtype SET[Elt : ELEM].
+Module Type SET[Elt : ELEM].
   Parameter T : Set.
   Parameter empty : T.
   Parameter add : Elt.T -> T -> T.
@@ -50,9 +50,9 @@ Modtype SET[Elt : ELEM].
         (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> 
 	(find e (add e' s))=(find e s).
 
-EndT SET.
+End SET.
 
-Mod 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').
@@ -93,20 +93,20 @@ Mod FuncDict[E : ELEM].
 
   Qed.
 
-EndM FuncDict.
+End FuncDict.
 
-Mod F : SET := FuncDict.
+Module F : SET := FuncDict.
 
 
-Mod Nat.
+Module Nat.
   Definition T:=nat.
   Lemma eq_dec :  (a,a':T){a=a'}+{~ a=a'}.
     Decide Equality.
   Qed.
-EndM Nat.
+End Nat.
 
 
-Mod SetNat:=F Nat. 
+Module SetNat:=F Nat. 
 
 
 Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. 
@@ -114,9 +114,9 @@ Apply SetNat.find_empty_false.
 Save.
 
 (***************************************************************************)
-Mod Lemmas[G:SET][E:ELEM].
+Module Lemmas[G:SET][E:ELEM].
 
-  Mod 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 
@@ -132,13 +132,13 @@ Mod Lemmas[G:SET][E:ELEM].
        Try (Rewrite ESet.find_add_false; Auto); 
        Auto).
   Save.
-EndM Lemmas.
+End Lemmas.
 
 
 Inductive list [A:Set] : Set := nil : (list A) 
                              | cons : A -> (list A) -> (list A).
 
-Mod ListDict[E : ELEM]. 
+Module ListDict[E : ELEM]. 
   Definition T := (list E.T).
   Definition elt := E.T.
    
@@ -179,10 +179,10 @@ Mod ListDict[E : ELEM].
   Save.    
   
 
-EndM ListDict.
+End ListDict.
 
 
-Mod L : SET := ListDict.
+Module L : SET := ListDict.
 
 
 
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
index b14c3f793..0f8eef847 100644
--- a/test-suite/modules/fun_objects.v
+++ b/test-suite/modules/fun_objects.v
@@ -1,29 +1,29 @@
 Implicit Arguments On.
 
-Modtype SIG.
+Module Type SIG.
   Parameter id:(A:Set)A->A.
-EndT SIG.
+End SIG.
  
-Mod M[X:SIG].
+Module M[X:SIG].
   Definition idid := (X.id X.id).
   Definition id := (idid X.id).
-EndM M.
+End M.
 
-Mod N:=M.
+Module N:=M.
 
-Mod Nat.
+Module Nat.
   Definition T := nat.
   Definition x := O.
   Definition id := [A:Set][x:A]x.
-EndM Nat.
+End Nat.
 
-Mod Z:=(N Nat).
+Module Z:=(N Nat).
 
 Check (Z.idid O).
 
-Mod P[Y:SIG] := N.
+Module P[Y:SIG] := N.
 
-Mod Y:=P Nat Z.
+Module Y:=P Nat Z.
 
 Check (Y.id O).
 
diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v
index 7751e9f38..fb734b5d5 100644
--- a/test-suite/modules/grammar.v
+++ b/test-suite/modules/grammar.v
@@ -1,15 +1,15 @@
-Mod N.
+Module N.
 Definition f:=plus.
 Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
 Check (f O O).
-EndM N.
+End N.
 Check (N.f O O).
-Imp N.
+Import N.
 Check (N.f O O).
 Check (f O O).
-Mod M:=N.
+Module M:=N.
 Check (f O O).
 Check (N.f O O).
-Imp M.
+Import M.
 Check (f O O).
 Check (N.f O O).
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index ba333c525..5612ea755 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -1,4 +1,4 @@
-Mod M.
+Module M.
   Parameter rel:nat -> nat -> Prop.
 
   Axiom w : (n:nat)(rel O (S n)).
@@ -14,13 +14,13 @@ Mod M.
   Auto.
   Save.
 
-EndM M.
+End M.
 
 (*Lemma w1 : (M.rel O (S O)).
 Auto.
 *)
 
-Imp M.
+Import M.
 
 Print Hint *.
 Lemma w1 : (O#(S O)).
@@ -35,5 +35,5 @@ Locate rel.
 
 Locate M.
 
-Mod N:=Scratch.M.
+Module N:=Top.M.
 
diff --git a/test-suite/modules/modulik.v b/test-suite/modules/modulik.v
deleted file mode 100644
index 50d985e52..000000000
--- a/test-suite/modules/modulik.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Definition toto := Set.
-
-Mod M.
-  Definition id:=[X:Set]X.
-EndM M.
diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
index b02bdf189..2231e0849 100644
--- a/test-suite/modules/obj.v
+++ b/test-suite/modules/obj.v
@@ -1,26 +1,26 @@
 Implicit Arguments On.
 
-Mod M. 
+Module M. 
   Definition a:=[s:Set]s.
   Print a.
-EndM M.
+End M.
 
 Print M.a.
 
-Mod K.
+Module K.
   Definition app:=[A,B:Set; f:(A->B); x:A](f x).
-  Mod N.
+  Module N.
     Definition apap:=[A,B:Set](app (app 1!A 2!B)).
     Print app.
     Print apap.
-  EndM N.
+  End N.
   Print N.apap.
-EndM K.
+End K.
 
 Print K.app.
 Print K.N.apap.
 
-Mod 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 8183c67c6..c2d1c52dd 100644
--- a/test-suite/modules/objects.v
+++ b/test-suite/modules/objects.v
@@ -1,32 +1,32 @@
 Reset Initial.
 
-Modtype SET.
+Module Type SET.
   Axiom T:Set.
   Axiom x:T.
-EndT SET.
+End SET.
  
 Implicit Arguments On.
 
-Mod M[X:SET].
+Module M[X:SET].
   Definition T := nat.
   Definition x := O.
   Definition f := [A:Set][x:A]X.x.
-EndM M.
+End M.
 
-Mod N:=M.
+Module N:=M.
 
-Mod Nat.
+Module Nat.
   Definition T := nat.
   Definition x := O.
-EndM Nat.
+End Nat.
 
-Mod Z:=(N Nat).
+Module Z:=(N Nat).
 
 Check (Z.f O).
 
-Mod P[Y:SET] := N.
+Module P[Y:SET] := N.
 
-Mod Y:=P Z Nat.
+Module Y:=P Z Nat.
 
 Check (Y.f O).
 
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
index f800dec52..73fd6f322 100644
--- a/test-suite/modules/sub_objects.v
+++ b/test-suite/modules/sub_objects.v
@@ -3,33 +3,33 @@ Reset Initial.
 Set Implicit Arguments.
 
 
-Mod M.
+Module M.
   Definition id:=[A:Set][x:A]x.
 
-  Modtype SIG.
+  Module Type SIG.
     Parameter idid:(A:Set)A->A.
-  EndT SIG.
+  End SIG.
 
-  Mod N.
+  Module N.
     Definition idid:=[A:Set][x:A](id x).
     Grammar constr constr8 := 
       not_eq [ "#"  constr7($b) ] -> [ (idid $b) ].
     Syntactic Definition inc := (plus (S O)). 
-  EndM N.
+  End N.
 
   Definition zero:=(N.idid O).
 
-EndM M.
+End M.
 
 Definition zero := (M.N.idid O).
 Definition jeden := (M.N.inc O).
 
-Mod Goly:=M.N.
+Module Goly:=M.N.
 
 Definition Gole_zero := (Goly.idid O).
 Definition Goly_jeden := (Goly.inc O).
 
-Mod Ubrany : M.SIG := M.N.
+Module Ubrany : M.SIG := M.N.
 
 Definition Ubrane_zero := (Ubrany.idid O).