Encore quelques rangements dans Nametab + petits trucs

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

5 files changed, 218 insertions, 114 deletions

diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v
index 9773bc6f4..61966c7c8 100644
--- a/test-suite/modules/Nametab.v
+++ b/test-suite/modules/Nametab.v
@@ -1,128 +1,48 @@
 Module Q.
-Module N.
-Module K.
-Definition id:=Set.
-End K.
-End N.
+  Module N.
+    Module K.
+      Definition id:=Set.
+    End K.
+  End N.
 End Q.
 
-Locate id.
-Locate K.id.
-Locate N.K.id.
-Locate Q.N.K.id.
-Locate Top.Q.N.K.id.
-Locate K.
-Locate N.K.
-Locate Q.N.K.
-Locate Top.Q.N.K.
-Locate N.
-Locate Q.N.
-Locate Top.Q.N.
-Locate Q.
-Locate Top.Q.
+(* Bad *) Locate id.
+(* Bad *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
 
+(* Bad *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
 
-Module Type SIG.
-End SIG.
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
 
-Module Type FSIG[X:SIG].
-End FSIG.
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
 
-Module F[X:SIG].
-End F.
 
-(*
-#trace Nametab.push;;
-#trace Nametab.push_short_name;;
-#trace Nametab.freeze;;
-#trace Nametab.unfreeze;;
-#trace Nametab.exists_cci;;
-*)
 
-Module M.
-Reset M.
-Module M[X:SIG].
-Reset M.
-Module M[X,Y:SIG].
-Reset M.
-Module M[X:SIG;Y:SIG].
-Reset M.
-Module M[X,Y:SIG;Z1,Z:SIG].
-Reset M.
-Module M[X:SIG][Y: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.
-Reset M.
-Module M[X,Y:SIG;Z1,Z:SIG]:SIG.
-Reset M.
-Module M[X:SIG][Y:SIG]:SIG.
-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.
+Import Q.N.
 
 
-Module Type ELEM.
-  Parameter A:Set.
-  Parameter x:A.
-End ELEM.
+(* Bad *) Locate id.
+(* OK  *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
 
-Module Nat.
-    Definition A:=nat.
-    Definition x:=O.
-End Nat. 
+(* OK  *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
 
-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.
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
 
-  Definition singl := [x:X.A] (cons x nil).
-  
-  Lemma head_singl : (x:X.A)(head (singl x))=x.
-  Auto.
-  Qed.
-
-End List.
-
-Module N:=(List Nat).
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
new file mode 100644
index 000000000..13c284181
--- /dev/null
+++ b/test-suite/modules/Tescik.v
@@ -0,0 +1,30 @@
+
+Module Type ELEM.
+  Parameter A:Set.
+  Parameter x:A.
+End ELEM.
+
+Module Nat.
+    Definition A:=nat.
+    Definition x:=O.
+End Nat. 
+
+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 singl := [x:X.A] (cons x nil).
+  
+  Lemma head_singl : (x:X.A)(head (singl x))=x.
+  Auto.
+  Qed.
+
+End List.
+
+Module N:=(List Nat).
diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
new file mode 100644
index 000000000..505821d7e
--- /dev/null
+++ b/test-suite/output/Nametab.out
@@ -0,0 +1,28 @@
+id is not a defined object
+K.id is not a defined object
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+K is not a defined object
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
+id is not a defined object
+Constant Top.Q.N.K.id
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+Module Top.Q.N.K
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v
new file mode 100644
index 000000000..61966c7c8
--- /dev/null
+++ b/test-suite/output/Nametab.v
@@ -0,0 +1,48 @@
+Module Q.
+  Module N.
+    Module K.
+      Definition id:=Set.
+    End K.
+  End N.
+End Q.
+
+(* Bad *) Locate id.
+(* Bad *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
+
+(* Bad *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
+
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
+
+
+
+Import Q.N.
+
+
+(* Bad *) Locate id.
+(* OK  *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
+
+(* OK  *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
+
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v
new file mode 100644
index 000000000..098de3cfb
--- /dev/null
+++ b/test-suite/success/Mod_params.v
@@ -0,0 +1,78 @@
+(* Syntax test - all possible kinds of module parameters *)
+
+Module Type SIG.
+End SIG.
+
+Module Type FSIG[X:SIG].
+End FSIG.
+
+Module F[X:SIG].
+End F.
+
+Module Q.
+End Q.
+
+(*
+#trace Nametab.push;;
+#trace Nametab.push_short_name;;
+#trace Nametab.freeze;;
+#trace Nametab.unfreeze;;
+#trace Nametab.exists_cci;;
+*)
+
+Module M.
+Reset M.
+Module M[X:SIG].
+Reset M.
+Module M[X,Y:SIG].
+Reset M.
+Module M[X:SIG;Y:SIG].
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG].
+Reset M.
+Module M[X:SIG][Y: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.
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG]:SIG.
+Reset M.
+Module M[X:SIG][Y:SIG]:SIG.
+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.