[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>

6 files changed, 28 insertions, 27 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5336948642..b12364d04a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
 
 let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
-  let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in
-  let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in
-  let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in
+  let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in
+  let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in
+  let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -1605,7 +1605,7 @@ let prove_principle_for_gen
     match !tcc_lemma_ref with
      | Undefined -> user_err Pp.(str "No tcc proof !!")
      | Value lemma -> EConstr.of_constr lemma
-     | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ())
+     | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I")
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0c45de4dc4..7c80b776a4 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -259,11 +259,8 @@ let mk_result ctxt value avoid =
   Some functions to deal with overlapping patterns
 **************************************************)
 
-let coq_True_ref =
-  lazy  (Coqlib.coq_reference "" ["Init";"Logic"] "True")
-
-let coq_False_ref =
-  lazy  (Coqlib.coq_reference "" ["Init";"Logic"] "False")
+let coq_True_ref  = lazy (Coqlib.lib_ref "core.True.type")
+let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type")
 
 (*
   [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
@@ -957,7 +954,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			assert false
 		end
 	    | GApp(eq_as_ref,[ty; id ;rt])
-		when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
+                when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type")  && n == Anonymous
 		  ->
                 let loc1 = rt.CAst.loc in
                 let loc2 = eq_as_ref.CAst.loc in
@@ -1078,7 +1075,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     else new_b, Id.Set.add id id_to_exclude
 		  *)
 	    | GApp(eq_as_ref,[ty;rt1;rt2])
-		when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
+                when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous
 		  ->
 	      begin
 		try 
@@ -1089,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      List.fold_left 
 			(fun acc (lhs,rhs) -> 
 			  mkGProd(Anonymous,
-				  mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc)
+                                  mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc)
 			)
 			b
 			l
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index f81de82d5e..5b45a8dbed 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -38,11 +38,11 @@ let glob_decompose_app =
 
 (* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *)
 let glob_make_eq ?(typ= mkGHole ()) t1 t2  =
-  mkGApp(mkGRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
+  mkGApp(mkGRef (Coqlib.lib_ref "core.eq.type"),[typ;t2;t1])
 
 (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
 let glob_make_neq t1 t2 =
-  mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2])
+  mkGApp(mkGRef (Coqlib.lib_ref "core.not.type"),[glob_make_eq t1 t2])
 
 let remove_name_from_mapping mapping na =
   match na with
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6ed382ca1c..03a64988e4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -114,6 +114,7 @@ let def_of_const t =
        with Not_found -> assert false)
     |_ -> assert false
 
+[@@@ocaml.warning "-3"]
 let coq_constant s =
   UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "RecursiveDefinition"
@@ -441,7 +442,7 @@ let jmeq () =
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
     UnivGen.constr_of_global @@
-      Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
+      Coqlib.lib_ref "core.JMeq.type"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
@@ -449,7 +450,7 @@ let jmeq_refl () =
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
     UnivGen.constr_of_global @@
-      Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
+      Coqlib.lib_ref "core.JMeq.refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
@@ -461,8 +462,10 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded"
 let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
 let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
 
+[@@@ocaml.warning "-3"]
 let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
-    Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
+    Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
+[@@@ocaml.warning "+3"]
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 56fe430077..b8973a18dc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -81,10 +81,9 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 let make_eq () =
   try
-    EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ()))
-  with _ -> assert false 
+    EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type"))
+  with _ -> assert false
 
-	  
 (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
    (resp. g_to_f = false) where [graph]  is the graph of [f] and is the [i]th function in the block.
 
@@ -512,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
 			    intros_with_rewrite
 			  ] g
 			end
-                  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) ->
+                  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENLIST[
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 633d98a585..89dfb58017 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -49,11 +49,12 @@ open Context.Rel.Declaration
 
 (* Ugly things which should not be here *)
 
+[@@@ocaml.warning "-3"]
 let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
-  Coqlib.coq_reference "RecursiveDefinition" m s
+  Coqlib.find_reference "RecursiveDefinition" m s
 
-let arith_Nat = ["Arith";"PeanoNat";"Nat"]
-let arith_Lt = ["Arith";"Lt"]
+let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
+let arith_Lt  = ["Coq"; "Arith";"Lt"]
 
 let pr_leconstr_rd =
   let sigma, env = Pfedit.get_current_context () in
@@ -63,6 +64,7 @@ let coq_init_constant s =
   EConstr.of_constr (
     UnivGen.constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
+[@@@ocaml.warning "+3"]
 
 let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -143,6 +145,7 @@ let def_id = Id.of_string "def"
 let p_id = Id.of_string "p"
 let rec_res_id = Id.of_string "rec_res";;
 let lt = function () -> (coq_init_constant "lt")
+[@@@ocaml.warning "-3"]
 let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
 let ex = function () -> (coq_init_constant "ex")
 let nat = function () -> (coq_init_constant "nat")
@@ -163,7 +166,6 @@ let coq_S = function () -> (coq_init_constant "S")
 let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
 let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref))
-let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj"
 
 let f_S t = mkApp(delayed_force coq_S, [|t|]);;
 
@@ -1241,8 +1243,8 @@ let get_current_subgoals_types () =
 
 exception EmptySubgoals
 let build_and_l sigma l =
-  let and_constr =  UnivGen.constr_of_global @@ Coqlib.build_coq_and () in
-  let conj_constr = coq_conj () in
+  let and_constr =  UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in
+  let conj_constr = Coqlib.build_coq_conj () in
   let mk_and p1 p2 =
     mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
   let rec is_well_founded t =