diff options
| author | coq | 2003-01-09 16:22:35 +0000 |
|---|---|---|
| committer | coq | 2003-01-09 16:22:35 +0000 |
| commit | 24d8bd2814c9ef89d918ce81d5a0d30fe0662335 (patch) | |
| tree | 548688c4f8ef82c399b29efc93102418c750fc17 /test-suite | |
| parent | c8bfdc5661063b707e6ec8035ea9b3305871059a (diff) | |
Export M + Module M <: SIG
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/TranspModtype.out | 7 | ||||
| -rw-r--r-- | test-suite/output/TranspModtype.v | 22 |
2 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out new file mode 100644 index 0000000000..f94ed64234 --- /dev/null +++ b/test-suite/output/TranspModtype.out @@ -0,0 +1,7 @@ +TrM.A = M.A + : Set +OpM.A = M.A + : Set +TrM.B = M.B + : Set +*** [ OpM.B : Set ] diff --git a/test-suite/output/TranspModtype.v b/test-suite/output/TranspModtype.v new file mode 100644 index 0000000000..27b1fb9f92 --- /dev/null +++ b/test-suite/output/TranspModtype.v @@ -0,0 +1,22 @@ +Module Type SIG. + Axiom A:Set. + Axiom B:Set. +End SIG. + +Module M:SIG. + Definition A:=nat. + Definition B:=nat. +End M. + +Module N<:SIG:=M. + +Module TranspId[X:SIG] <: SIG with Definition A:=X.A := X. +Module OpaqueId[X:SIG] : SIG with Definition A:=X.A := X. + +Module TrM := TranspId M. +Module OpM := OpaqueId M. + +Print TrM.A. +Print OpM.A. +Print TrM.B. +Print OpM.B. |