summaryrefslogtreecommitdiff
path: root/test-suite/output/TranspModtype.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/TranspModtype.out')
-rw-r--r--test-suite/output/TranspModtype.out8
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index f94ed642..67b65d4b 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,7 +1,15 @@
TrM.A = M.A
: Set
+
+TrM.A is not universe polymorphic
OpM.A = M.A
: Set
+
+OpM.A is not universe polymorphic
TrM.B = M.B
: Set
+
+TrM.B is not universe polymorphic
*** [ OpM.B : Set ]
+
+OpM.B is not universe polymorphic