diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index c18744052e..dfac78c048 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 @@ -57,7 +58,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = declare_global_definition ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~univs ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) |