diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 980db4109..dfac78c04 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps = let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in - let () = Universes.register_universe_binders gr pl in + let () = Declare.declare_univ_binders gr pl in let () = definition_message ident in gr @@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = let () = definition_message ident in let gr = VarRef ident in let () = maybe_declare_manual_implicits false gr imps in + let () = Declare.declare_univ_binders gr pl in let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in |