diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-21 11:14:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | d071eac98b7812ac5c03004b438022900885d874 (patch) | |
| tree | f0f72dba7daf7c91ea2eda0332b568c4615ad3c9 /test-suite/output | |
| parent | 765392492df2f5e065b2b5e706b6620846337cc0 (diff) | |
Forbid repeated names in universe binders.
Diffstat (limited to 'test-suite/output')
| -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. *) |