diff options
Diffstat (limited to 'test-suite/output/Load.out')
| -rw-r--r-- | test-suite/output/Load.out | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out index 0904d5540b..f84cedfa62 100644 --- a/test-suite/output/Load.out +++ b/test-suite/output/Load.out @@ -1,6 +1,10 @@ -f = 2 +Monomorphic f = 2 : nat -u = I + +f is not universe polymorphic +Monomorphic u = I : True + +u is not universe polymorphic The command has indeed failed with message: Files processed by Load cannot leave open proofs. |