1 files changed, 6 insertions, 6 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index d7a4fcca3d..dfac78c048 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -11,18 +11,17 @@ open Declare
 open Entries
 open Globnames
 open Impargs
-open Nameops
 
 let warn_definition_not_visible =
   CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
     Pp.(fun ident ->
         strbrk "Section definition " ++
-        pr_id ident ++ strbrk " is not visible from current goals")
+        Names.Id.print ident ++ strbrk " is not visible from current goals")
 
 let warn_local_declaration =
   CWarnings.create ~name:"local-declaration" ~category:"scope"
     Pp.(fun (id,kind) ->
-        pr_id id ++ strbrk " is declared as a local " ++ str kind)
+        Names.Id.print id ++ strbrk " is declared as a local " ++ str kind)
 
 let get_locality id ~kind = function
 | Discharge ->
@@ -37,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
 
@@ -50,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
@@ -58,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))