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

4 files changed, 14 insertions, 12 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index f2f236f448..1492cfb4e4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -201,8 +201,8 @@ let mkRInd mind = DAst.make @@ GRef (IndRef mind,None)
 let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
 let rec mkRnat n =
-  if n <= 0 then DAst.make @@ GRef (Coqlib.glob_O, None) else
-  mkRApp (DAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)]
+  if n <= 0 then DAst.make @@ GRef (Coqlib.lib_ref "num.nat.O", None) else
+  mkRApp (DAst.make @@ GRef (Coqlib.lib_ref "num.nat.S", None)) [mkRnat (n - 1)]
 
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -763,7 +763,7 @@ let mkEtaApp c n imin =
 
 let mkRefl t c gl =
   let sigma = project gl in
-  let (sigma, refl) = EConstr.fresh_global (pf_env gl) sigma Coqlib.((build_coq_eq_data()).refl) in
+  let (sigma, refl) = EConstr.fresh_global (pf_env gl) sigma Coqlib.(lib_ref "core.eq.refl") in
   EConstr.mkApp (refl, [|t; c|]), { gl with sigma }
 
 let discharge_hyp (id', (id, mode)) gl =
@@ -1220,7 +1220,7 @@ let genclrtac cl cs clr =
       (fun type_err gl ->
          tclTHEN
            (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
-             (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
+             (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr))
            (fun gl -> raise type_err)
            gl))
     (old_cleartac clr)
@@ -1504,7 +1504,7 @@ let tclOPTION o d =
 let tacIS_INJECTION_CASE ?ty t = begin
   tclOPTION ty (tacTYPEOF t) >>= fun ty ->
   tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) ->
-  tclUNIT (GlobRef.equal (GlobRef.IndRef mind) (Coqlib.build_coq_eq ()))
+  tclUNIT (Coqlib.check_ind_ref "core.eq.type" mind)
 end
 
 let tclWITHTOP tac = Goal.enter begin fun gl ->
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 602fcfcab5..7f9a9e125e 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -115,7 +115,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
   let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in
   ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM==")));
   let fire_subst gl t = Reductionops.nf_evar (project gl) t in
-  let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
+  let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
   let eq = EConstr.of_constr eq in
   let is_undef_pat = function
   | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t)
@@ -421,7 +421,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with
 let is_injection_case c gl =
   let gl, cty = pfe_type_of gl c in
   let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in
-  GlobRef.equal (IndRef mind) (Coqlib.build_coq_eq ())
+  GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type")
 
 let perform_injection c gl =
   let gl, cty = pfe_type_of gl c in
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 2af917b939..c04ced4ab4 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -130,7 +130,7 @@ let newssrcongrtac arg ist gl =
   let ssr_congr lr = EConstr.mkApp (arr, lr) in
   (* here thw two cases: simple equality or arrow *)
   let equality, _, eq_args, gl' =
-    let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
+    let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
     pf_saturate gl (EConstr.of_constr eq) 3 in
   tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
   (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
@@ -386,7 +386,7 @@ let rwcltac cl rdx dir sr gl =
         ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr)));
   let cvtac, rwtac, gl =
     if EConstr.Vars.closed0 (project gl) r' then 
-      let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in
+      let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
@@ -427,6 +427,7 @@ let rwcltac cl rdx dir sr gl =
 ;;
 
 
+[@@@ocaml.warning "-3"]
 let lz_coq_prod =
   let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod
 
@@ -438,7 +439,7 @@ let lz_setoid_relation =
   | _ ->
     let srel =
        try Some (UnivGen.constr_of_global @@
-                   Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation")
+                 Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
        with _ -> None in
     last_srel := (env, srel); srel
 
@@ -484,7 +485,7 @@ let rwprocess_rule dir rule gl =
           | _ ->
             let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
             EConstr.mkApp (pi2, ra), sigma in
-        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then
+        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then
          let s, sigma = sr sigma 2 in
          loop (converse_dir d) sigma s a.(1) rs 0
         else
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 1dbacf0ff7..ce439d0497 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -149,6 +149,7 @@ let tac_case t =
 end
 
 (** [=> [: id]] ************************************************************)
+[@@@ocaml.warning "-3"]
 let mk_abstract_id =
   let open Coqlib in
   let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in
@@ -375,7 +376,7 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
        let rec gen_eq_tac () = Goal.enter begin fun g ->
          let sigma, env, concl = Goal.(sigma g, env g, concl g) in
          let sigma, eq =
-           EConstr.fresh_global env sigma (Coqlib.build_coq_eq ()) in
+           EConstr.fresh_global env sigma (Coqlib.lib_ref "core.eq.type") in
          let ctx, last = EConstr.decompose_prod_assum sigma concl in
          let args = match EConstr.kind_of_type sigma last with
            | Term.AtomicType (hd, args) ->