diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/TranspModtype.out | 10 | ||||
| -rw-r--r-- | test-suite/output/TranspModtype.v | 22 |
2 files changed, 0 insertions, 32 deletions
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out deleted file mode 100644 index 41e8648bc0..0000000000 --- a/test-suite/output/TranspModtype.out +++ /dev/null @@ -1,10 +0,0 @@ -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 deleted file mode 100644 index 27b1fb9f92..0000000000 --- a/test-suite/output/TranspModtype.v +++ /dev/null @@ -1,22 +0,0 @@ -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. |
