From 2069ddbed501da4f24203d3fb92187e012ab582d Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 27 Sep 2002 12:10:04 +0000
Subject: 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
---
 test-suite/success/Mod_params.v | 78 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 test-suite/success/Mod_params.v

(limited to 'test-suite/success')

diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v
new file mode 100644
index 0000000000..098de3cfbf
--- /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.
-- 
cgit v1.2.3