aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/TranspModtype.out
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-08 15:31:56 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-08 15:35:59 +0200
commit0cebd2b86a90cc1361bcfac6bb097540e22c9a21 (patch)
tree648ece59fd72185da10d71771d9f858aa1fa7fd4 /test-suite/output/TranspModtype.out
parent6a3767e48e91604071b5709a6658aa2f255a4522 (diff)
Fixing output test-suite: since universe polymorphism, the Print command
shows the polymorphism status of the term.
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 f94ed6423..dbbd73dcd 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 monomorphic
OpM.A = M.A
: Set
+
+OpM.A is monomorphic
TrM.B = M.B
: Set
+
+TrM.B is monomorphic
*** [ OpM.B : Set ]
+
+OpM.B is monomorphic