aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/TranspModtype.out
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-03-09 08:26:00 +0100
committerGuillaume Melquiond2015-03-09 08:26:00 +0100
commite4ad47fed594d6865f5bd29a159976cb072f0fae (patch)
tree893bd81fe7df422d7c0a2bd545650a1e7ca86268 /test-suite/output/TranspModtype.out
parentd337afac6f9b1fe405c89b4e62f660cadf171f0f (diff)
Do not display the status of monomorphic constants unless in universe-polymorphism mode.
Diffstat (limited to 'test-suite/output/TranspModtype.out')
-rw-r--r--test-suite/output/TranspModtype.out8
1 files changed, 0 insertions, 8 deletions
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 67b65d4b81..f94ed64234 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,15 +1,7 @@
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