[coqlib] Rebindable Coqlib namespace.

We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.

This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.

Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

10 files changed, 79 insertions, 88 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index dee7541d37..148d4437fa 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -62,29 +62,23 @@ exception NoDecidabilityCoInductive
 exception ConstructorWithNonParametricInductiveType of inductive
 exception DecidabilityIndicesNotSupported
 
-let constr_of_global g = lazy (UnivGen.constr_of_global g)
-
 (* Some pre declaration of constant we are going to use *)
-let bb = constr_of_global Coqlib.glob_bool
-
-let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
+let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop")
 
 let andb_true_intro = fun _ ->
   UnivGen.constr_of_global
-    (Coqlib.build_bool_type()).Coqlib.andb_true_intro
-
-let tt = constr_of_global Coqlib.glob_true
-
-let ff = constr_of_global Coqlib.glob_false
-
-let eq = constr_of_global Coqlib.glob_eq
-
-let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ())
+    (Coqlib.lib_ref "core.bool.andb_true_intro")
 
-let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
+(* We avoid to use lazy as the binding of constants can change *)
+let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type")
+let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true")
+let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false")
+let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")
 
-let induct_on c = induction false None c None None
+let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type")
+let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb")
 
+let induct_on  c = induction false None c None None
 let destruct_on c = destruct false None c None None
 
 let destruct_on_using c id =
@@ -119,7 +113,7 @@ let mkFullInd (ind,u) n =
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
-  try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in ()
+  try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in ()
   with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
 
 let check_no_indices mib =
@@ -160,7 +154,7 @@ let build_beq_scheme mode kn =
       let eqs_typ = List.map (fun aa ->
                                 let a = lift !lift_cnt aa in
                                   incr lift_cnt;
-                                  myArrow a (myArrow a (Lazy.force bb))
+                                  myArrow a (myArrow a (bb ()))
                              ) ext_rel_list in
 
         let eq_input = List.fold_left2
@@ -259,7 +253,7 @@ let build_beq_scheme mode kn =
      List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
       (mkLambda (Anonymous,
                  mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
-                 (Lazy.force bb)))
+                 (bb ())))
       (List.rev rettyp_l) in
   (* make_one_eq *)
   (* do the [| C1 ... =>  match Y with ... end
@@ -270,17 +264,17 @@ let build_beq_scheme mode kn =
       Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
-    let ar = Array.make n (Lazy.force ff) in
+    let ar = Array.make n (ff ()) in
     let eff = ref Safe_typing.empty_private_constants in
 	for i=0 to n-1 do
 	  let nb_cstr_args = List.length constrsi.(i).cs_args in
-	  let ar2 = Array.make n (Lazy.force ff) in
+          let ar2 = Array.make n (ff ()) in
           let constrsj = constrs (3+nparrec+nb_cstr_args) in
 	    for j=0 to n-1 do
 	      if Int.equal i j then
 		ar2.(j) <- let cc = (match nb_cstr_args with
-                    | 0 -> Lazy.force tt
-                    | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
+                    | 0 -> tt ()
+                    | _ -> let eqs = Array.make nb_cstr_args (tt ()) in
                       for ndx = 0 to nb_cstr_args-1 do
                         let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
                           let eqA, eff' = compute_A_equality rel_list
@@ -305,7 +299,7 @@ let build_beq_scheme mode kn =
                     (constrsj.(j).cs_args)
 		)
 	      else ar2.(j) <- (List.fold_left (fun a decl ->
-			mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
+                        mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (ff ())  (constrsj.(j).cs_args) )
 	    done;
 
 	  ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a))
@@ -326,7 +320,7 @@ let build_beq_scheme mode kn =
     for i=0 to (nb_ind-1) do
         names.(i) <- Name (Id.of_string (rec_name i));
 	types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0)
-                     (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb));
+                     (mkArrow (mkFullInd ((kn,i),u) 1) (bb ()));
         let c, eff' = make_one_eq i in
         cores.(i) <- c;
         eff := Safe_typing.concat_private eff' !eff
@@ -570,15 +564,15 @@ let compute_bl_goal ind lnamesparrec nparrec =
         mkNamedProd x (mkVar s) (
             mkNamedProd y (mkVar s) (
               mkArrow
-               ( mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(mkVar seq,[|mkVar x;mkVar y|]);(Lazy.force tt)|]))
-               ( mkApp(Lazy.force eq,[|mkVar s;mkVar x;mkVar y|]))
+               ( mkApp(eq (),[|bb (); mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt () |]))
+               ( mkApp(eq (),[|mkVar s;mkVar x;mkVar y|]))
           ))
         ) list_id in
       let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
         mkNamedProd sbl b a
       ) c (List.rev list_id) (List.rev bl_typ) in
       let eqs_typ = List.map (fun (s,_,_,_) ->
-          mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(Lazy.force bb)))
+          mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(bb ())))
           ) list_id in
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
         mkNamedProd seq b a
@@ -594,8 +588,8 @@ let compute_bl_goal ind lnamesparrec nparrec =
         mkNamedProd n (mkFullInd (ind,u) nparrec) (
           mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
             mkArrow
-              (mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(eqI,[|mkVar n;mkVar m|]);(Lazy.force tt)|]))
-              (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
+              (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
+              (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
         ))), eff
 
 let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
@@ -651,7 +645,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                         | App (c,ca) -> (
                           match EConstr.kind sigma c with
                           | Ind (indeq, u) ->
-                              if GlobRef.equal (IndRef indeq) Coqlib.glob_eq
+                              if GlobRef.equal (IndRef indeq) Coqlib.(lib_ref "core.eq.type")
                               then
                                 Tacticals.New.tclTHEN
                                   (do_replace_bl mode bl_scheme_key ind
@@ -704,7 +698,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
 
 let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
-  let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
+  let eq = eq () and tt = tt () and bb = bb () in
   let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
   let eqI, eff = eqI ind lnamesparrec in
     let create_input c =
@@ -827,13 +821,13 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
 (* Decidable equality *)
 
 let check_not_is_defined () =
-  try ignore (Coqlib.build_coq_not ())
-  with e when CErrors.noncritical e -> raise (UndefinedCst "not")
+  try ignore (Coqlib.lib_ref "core.not.type")
+  with Not_found -> raise (UndefinedCst "not")
 
 (* {n=m}+{n<>m}  part  *)
 let compute_dec_goal ind lnamesparrec nparrec =
   check_not_is_defined ();
-  let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
+  let eq = eq () and tt = tt () and bb = bb () in
   let list_id = list_id lnamesparrec in
   let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
     let create_input c =
@@ -879,14 +873,14 @@ let compute_dec_goal ind lnamesparrec nparrec =
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (
             mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
-              mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
+              mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
           )
         )
       )
 
 let compute_dec_tact ind lnamesparrec nparrec =
-  let eq = Lazy.force eq and tt = Lazy.force tt 
-  and ff = Lazy.force ff and bb = Lazy.force bb in
+  let eq = eq () and tt = tt ()
+  and ff = ff () and bb = bb () in
   let list_id = list_id lnamesparrec in
   let eqI, eff = eqI ind lnamesparrec in
   let avoid = ref [] in
@@ -949,7 +943,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
             let freshH3 = fresh_id (Id.of_string "H") gl in
             Tacticals.New.tclTHENLIST [
 	      simplest_right ;
-              unfold_constr (Lazy.force Coqlib.coq_not_ref);
+              unfold_constr (Coqlib.lib_ref "core.not.type");
               intro;
               Equality.subst_all ();
               assert_by (Name freshH3)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 04cd4173a8..5f340dc144 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -160,14 +160,8 @@ type recursive_preentry =
 
 (* Wellfounded definition *)
 
-let contrib_name = "Program"
-let subtac_dir = [contrib_name]
-let tactics_module = subtac_dir @ ["Tactics"]
-
-let init_constant dir s sigma =
-  Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)
-
-let fix_proto = init_constant tactics_module "fix_proto"
+let fix_proto sigma =
+  Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto")
 
 let interp_recursive ~program_mode ~cofix fixl notations =
   let open Context.Named.Declaration in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 102a98f046..c33e6b72c6 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -23,27 +23,16 @@ module RelDecl = Context.Rel.Declaration
 
 open Coqlib
 
-let contrib_name = "Program"
-let subtac_dir = [contrib_name]
-let fixsub_module = subtac_dir @ ["Wf"]
-(* let tactics_module = subtac_dir @ ["Tactics"] *)
+let init_constant sigma rf = Evarutil.new_global sigma rf
+let fix_sub_ref () = lib_ref "program.wf.fix_sub"
+let measure_on_R_ref () = lib_ref "program.wf.mr"
+let well_founded sigma = init_constant sigma (lib_ref "core.wf.well_founded")
 
-let init_reference dir s () = Coqlib.coq_reference "Command" dir s
-let init_constant dir s sigma =
-  Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)
-
-let make_ref l s = init_reference l s
-(* let fix_proto = init_constant tactics_module "fix_proto" *)
-let fix_sub_ref = make_ref fixsub_module "Fix_sub"
-let measure_on_R_ref = make_ref fixsub_module "MR"
-let well_founded = init_constant ["Init"; "Wf"] "well_founded"
 let mkSubset sigma name typ prop =
   let open EConstr in
   let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in
   sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |])
 
-let sigT = Lazy.from_fun build_sigma_type
-
 let make_qref s = qualid_of_string s
 let lt_ref = make_qref "Init.Peano.lt"
 
@@ -60,8 +49,8 @@ let rec telescope sigma l =
           (fun (sigma, ty, tys, (k, constr)) decl ->
             let t = RelDecl.get_type decl in
             let pred = mkLambda (RelDecl.get_name decl, t, ty) in
-            let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in
-            let sigma, intro = Evarutil.new_global sigma (Lazy.force sigT).intro in
+            let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in
+            let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in
             let sigty = mkApp (ty, [|t; pred|]) in
             let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
               (sigma, sigty, pred :: tys, (succ k, intro)))
@@ -70,8 +59,8 @@ let rec telescope sigma l =
       let sigma, last, subst = List.fold_right2
         (fun pred decl (sigma, prev, subst) ->
           let t = RelDecl.get_type decl in
-          let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in
-          let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in
+          let sigma, p1 = Evarutil.new_global sigma (lib_ref "core.sigT.proj1") in
+          let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in
           let proj1 = applist (p1, [t; pred; prev]) in
           let proj2 = applist (p2, [t; pred; prev]) in
             (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 895737b538..d7229d32fe 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -212,7 +212,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
       | IDENT "Register"; g = global; "as"; quid = qualid ->
-          { VernacRegister(g, RegisterRetroknowledge quid) }
+          { VernacRegister(g, RegisterCoqlib quid) }
       | IDENT "Register"; IDENT "Inline"; g = global ->
           { VernacRegister(g, RegisterInline) }
       | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
@@ -994,7 +994,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) }
       | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, true, qid) }
       | IDENT "Strategy"; qid = smart_global -> { PrintStrategy (Some qid) }
-      | IDENT "Strategies" -> { PrintStrategy None } ] ]
+      | IDENT "Strategies" -> { PrintStrategy None }
+      | IDENT "Registered" -> { PrintRegistered }
+    ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> { FunClass }
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b354ad0521..5f2818c12b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -451,11 +451,11 @@ let fold_left' f = function
     [] -> invalid_arg "fold_left'"
   | hd :: tl -> List.fold_left f hd tl
 
-let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ())
-let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ())
+let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.and.type")
+let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.and.conj")
 
-let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.build_coq_prod ())
-let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.build_coq_pair ())
+let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.type")
+let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.intro")
 
 let build_combined_scheme env schemes =
   let evdref = ref (Evd.from_env env) in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c4a10b4be6..757a56d436 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -256,11 +256,9 @@ let eterm_obligations env name evm fs ?status t ty =
   let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
     Array.of_list (List.rev evars), (evnames, evmap), t', ty
 
-let tactics_module = ["Program";"Tactics"]
-let safe_init_constant md name () =
-  Coqlib.check_required_library ("Coq"::md);
-  UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name)
-let hide_obligation = safe_init_constant tactics_module "obligation"
+let hide_obligation () =
+  Coqlib.check_required_library ["Coq";"Program";"Tactics"];
+  UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation")
 
 let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
 let error s = pperror (str s)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b4b3aead91..a0e8f38c0b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -533,6 +533,8 @@ open Pputils
       keyword "Print Strategies"
     | PrintStrategy (Some qid) ->
       keyword "Print Strategy" ++ pr_smart_global qid
+    | PrintRegistered ->
+      keyword "Print Registered"
 
   let pr_using e =
     let rec aux = function
@@ -1159,14 +1161,16 @@ open Pputils
           | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
         in
         return (keyword "Locate" ++ spc() ++ pr_locate loc)
-      | VernacRegister (id, RegisterInline) ->
+      | VernacRegister (qid, RegisterCoqlib name) ->
         return (
           hov 2
-            (keyword "Register Inline" ++ spc() ++ pr_qualid id)
+            (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as"
+             ++ spc () ++ pr_qualid name)
         )
-      | VernacRegister (id, RegisterRetroknowledge n) ->
+      | VernacRegister (qid, RegisterInline) ->
         return (
-          hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n)
+          hov 2
+            (keyword "Register Inline" ++ spc() ++ pr_qualid qid)
         )
       | VernacComments l ->
         return (
diff --git a/vernac/search.ml b/vernac/search.ml
index e8ccec11ca..04dcb7d565 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -236,13 +236,13 @@ let search_pattern gopt pat mods pr_search =
 
 (** SearchRewrite *)
 
-let eq = Coqlib.glob_eq
+let eq () = Coqlib.(lib_ref "core.eq.type")
 
 let rewrite_pat1 pat =
-  PApp (PRef eq, [| PMeta None; pat; PMeta None |])
+  PApp (PRef (eq ()), [| PMeta None; pat; PMeta None |])
 
 let rewrite_pat2 pat =
-  PApp (PRef eq, [| PMeta None; PMeta None; pat |])
+  PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |])
 
 let search_rewrite gopt pat mods pr_search =
   let pat1 = rewrite_pat1 pat in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index cf2fecb9c1..76f42db34d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -311,6 +311,13 @@ let print_strategy r =
     let lvl = get_strategy oracle key in
     pr_strategy (r, lvl)
 
+let print_registered () =
+  let pr_lib_ref (s,r) =
+    pr_global r ++ str " registered as " ++ str s
+  in
+  hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
+
+
 let dump_universes_gen g s =
   let output = open_out s in
   let output_constraint, close =
@@ -1866,6 +1873,7 @@ let vernac_print ~atts env sigma =
 	Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
       Printer.pr_assumptionset env sigma nassums
   | PrintStrategy r -> print_strategy r
+  | PrintRegistered -> print_registered ()
 
 let global_module qid =
   try Nametab.full_name_module qid
@@ -1972,14 +1980,14 @@ let vernac_register qid r =
     if not (isConstRef gr) then
       user_err Pp.(str "Register inline: a constant is expected");
     Global.register_inline (destConstRef gr)
-  | RegisterRetroknowledge n ->
+  | RegisterCoqlib n ->
     let path, id = Libnames.repr_qualid n in
     if DirPath.equal path Retroknowledge.int31_path
     then
       let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in
       Global.register f gr
     else
-      user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path))
+      Coqlib.register_ref (Libnames.string_of_qualid n) gr
 
 (********************)
 (* Proof management *)
@@ -2226,7 +2234,7 @@ let interp ?proof ~atts ~st c =
   | VernacSearch (s,g,r) -> vernac_search ~atts s g r
   | VernacLocate l ->
     Feedback.msg_notice @@ vernac_locate l
-  | VernacRegister (id, r) -> vernac_register id r
+  | VernacRegister (qid, r) -> vernac_register qid r
   | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
@@ -2278,6 +2286,7 @@ let check_vernac_supports_locality c l =
     | VernacSetOption _ | VernacUnsetOption _
     | VernacDeclareReduction _
     | VernacExtend _ 
+    | VernacRegister _
     | VernacInductive _) -> ()
   | Some _, _ -> user_err Pp.(str "This command does not support Locality")
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index a2ea706b75..27b485d94d 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -57,6 +57,7 @@ type printable =
   | PrintImplicit of qualid or_by_notation
   | PrintAssumptions of bool * bool * qualid or_by_notation
   | PrintStrategy of qualid or_by_notation option
+  | PrintRegistered
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
@@ -230,7 +231,7 @@ type extend_name =
    It will be extended with primitive inductive types and operators *)
 type register_kind =
   | RegisterInline
-  | RegisterRetroknowledge of qualid
+  | RegisterCoqlib of qualid
 
 (** {6 Types concerning the module layer} *)