diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-27 12:10:04 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-27 12:10:04 +0000 |
commit | 2069ddbed501da4f24203d3fb92187e012ab582d (patch) | |
tree | e29d9b1ec828157064f8b25e2e9167913f9f3298 /test-suite/success | |
parent | 6a9f037bad58c73aff5a972b36a2d5549ab37e71 (diff) |
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
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Mod_params.v | 78 |
1 files changed, 78 insertions, 0 deletions
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. |