diff options
| author | Gaëtan Gilbert | 2018-10-18 13:59:38 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-12 18:43:04 +0100 |
| commit | 7a3b6b644f85489dced02b33712ad21afe0df47d (patch) | |
| tree | 37cc8f21ec113ae70c2ac0c0c0cc09555ddeaa7e /test-suite | |
| parent | 81e7467a3db24887e1d4026ee8441846eb09309a (diff) | |
Don't declare universe binders for variables.
Otherwise
~~~
Unset Strict Universe Declaration.
Section bar.
Let baz := Type@{u}.
Definition k := baz.
End bar.
Section bar.
Let baz := Type@{u}.
Definition k' := baz.
End bar.
~~~
is broken (and has been since we stopped checking for repeated section names).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 5 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.v | 13 |
2 files changed, 5 insertions, 13 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 178116c580..2501ce4f26 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -79,8 +79,9 @@ mono The command has indeed failed with message: Universe u already exists. Monomorphic bobmorane = -let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff - : Type@{max(tt.u,ff.u)} +let tt := Type@{UnivBinders.32} in +let ff := Type@{UnivBinders.34} in tt -> ff + : Type@{max(UnivBinders.31,UnivBinders.33)} bobmorane is not universe polymorphic The command has indeed failed with message: diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 19d241d35d..ee3574341f 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -73,19 +73,10 @@ Module SecLet. (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) Unset Strict Universe Declaration. Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) - Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *) + Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *) Definition bobmorane := tt -> ff. End foo. - Print bobmorane. (* - bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} = - let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff - : Type@{max(UnivBinders.15,ff.u)} - (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15 - ff.v < ff.u - *) - - bobmorane is universe polymorphic - *) + Print bobmorane. End SecLet. (* fun x x => foo is nonsense with local binders *) |