diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/UnivBinders.out | 2 | ||||
-rw-r--r-- | test-suite/output/UnivBinders.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 04bd169bd..a2857294b 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -53,6 +53,8 @@ Monomorphic mono = Type@{u} (* {u} |= *) mono is not universe polymorphic +The command has indeed failed with message: +Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1, M+1, N+1)} diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index f0a990986..013f215b5 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -34,6 +34,9 @@ Print foo. Monomorphic Definition mono@{u} := Type@{u}. Print mono. +(* fun x x => foo is nonsense with local binders *) +Fail Definition fo@{u u} := Type@{u}. + (* Using local binders for printing. *) Print foo@{E M N}. (* Underscores discard the name if there's one. *) |