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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/declareDef.ml | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 5 |
2 files changed, 7 insertions, 4 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 35fb18e292..2fe03a8ec5 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -43,9 +43,11 @@ let declare_definition ident (local, p, k) ce pl imps hook = | Discharge | Local | Global -> let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in - ConstRef kn in + let gr = ConstRef kn in + let () = Declare.declare_univ_binders gr pl in + gr + in let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in let () = definition_message ident in Lemmas.call_hook fix_exn hook local gr; gr diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 150f2c6ee9..3b041b7065 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -197,10 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in - ConstRef kn + let gr = ConstRef kn in + Declare.declare_univ_binders gr (UState.universe_binders uctx); + gr in definition_message id; - Declare.declare_univ_binders r (UState.universe_binders uctx); call_hook (fun exn -> exn) hook locality r with e when CErrors.noncritical e -> let e = CErrors.push e in |