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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index fe8fc7c969..005334abe4 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -525,7 +525,7 @@ let declare_univ_binders gr pl = let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> id + | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on an constructor reference") |