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

8 files changed, 75 insertions, 73 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index e12063fd44..bd95a62532 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -12,7 +12,6 @@ open Constr
 open EConstr
 open Hipattern
 open Tactics
-open Coqlib
 open Reductionops
 open Proofview.Notations
 
@@ -33,8 +32,8 @@ let absurd c =
     let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
     Proofview.Unsafe.tclEVARS sigma <*>
-    Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot ->
-    Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse ->
+    Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.not.type")) >>= fun coqnot ->
+    Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.False.type")) >>= fun coqfalse ->
     Tacticals.New.tclTHENLIST [
       elim_type coqfalse;
       Simple.apply (mk_absurd_proof coqnot t)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 832014a610..f2bc679aac 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -27,7 +27,6 @@ open Constr_matching
 open Hipattern
 open Proofview.Notations
 open Tacmach.New
-open Coqlib
 open Tactypes
 
 (* This file containts the implementation of the tactics ``Decide
@@ -269,9 +268,10 @@ let decideEquality rectype ops =
 (* The tactic Compare *)
 
 let compare c1 c2 =
-  pf_constr_of_global (build_coq_sumbool ()) >>= fun opc ->
-  pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc ->
-  pf_constr_of_global (build_coq_not ()) >>= fun notc ->
+  let open Coqlib in
+  pf_constr_of_global (lib_ref "core.sumbool.type") >>= fun opc ->
+  pf_constr_of_global (lib_ref "core.eq.type") >>= fun eqc ->
+  pf_constr_of_global (lib_ref "core.not.type") >>= fun notc ->
   Proofview.Goal.enter begin fun gl ->
   let rectype = pf_unsafe_type_of gl c1 in
   let ops = (opc,eqc,notc) in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index ea5ff4a6cb..16b94cd154 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -99,7 +99,7 @@ let my_it_mkLambda_or_LetIn_name s c =
 
 let get_coq_eq ctx =
   try
-    let eq = Globnames.destIndRef Coqlib.glob_eq in
+    let eq = Globnames.destIndRef (Coqlib.lib_ref "core.eq.type") in
     (* Do not force the lazy if they are not defined *)
     let eq, ctx = with_context_set ctx 
       (UnivGen.fresh_inductive_instance (Global.env ()) eq) in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 510f119229..3e3ef78c5d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -339,12 +339,17 @@ let jmeq_same_dom env sigma = function
 let find_elim hdcncl lft2rgt dep cls ot =
   Proofview.Goal.enter_one begin fun gl ->
   let sigma = project gl in
-  let is_global gr c = Termops.is_global sigma gr c in
+  let is_global_exists gr c =
+    Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c
+  in
   let inccl = Option.is_empty cls in
   let env = Proofview.Goal.env gl in
-  if (is_global Coqlib.glob_eq hdcncl ||
-      (is_global Coqlib.glob_jmeq hdcncl &&
-	 jmeq_same_dom env sigma ot)) && not dep
+  (* if (is_global Coqlib.glob_eq hdcncl || *)
+  (*     (is_global Coqlib.glob_jmeq hdcncl && *)
+  (*        jmeq_same_dom env sigma ot)) && not dep *)
+  if (is_global_exists "core.eq.type" hdcncl ||
+      (is_global_exists "core.JMeq.type" hdcncl
+       && jmeq_same_dom env sigma ot)) && not dep
   then
     let c = 
       match EConstr.kind sigma hdcncl with 
@@ -588,7 +593,7 @@ let classes_dirpath =
 
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
-  else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
+  else check_required_library ["Coq";"Setoids";"Setoid"]
 
 let check_setoid cl = 
   Option.fold_left
@@ -637,8 +642,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   | None ->
     tclFAIL 0 (str"Terms do not have convertible types")
   | Some evd ->
-    let e = build_coq_eq () in
-    let sym = build_coq_eq_sym () in
+    let e = lib_ref "core.eq.type" in
+    let sym = lib_ref "core.eq.sym" in
     Tacticals.New.pf_constr_of_global sym >>= fun sym ->
     Tacticals.New.pf_constr_of_global e >>= fun e ->
     let eq = applist (e, [t1;c1;c2]) in
@@ -930,9 +935,9 @@ let build_selector env sigma dirn c ind special default =
   let ans = Inductiveops.make_case_or_project env sigma indf ci p c (Array.of_list brl) in
   ans
 
-let build_coq_False () = pf_constr_of_global (build_coq_False ())
-let build_coq_True () = pf_constr_of_global (build_coq_True ())
-let build_coq_I () = pf_constr_of_global (build_coq_I ())
+let build_coq_False () = pf_constr_of_global (lib_ref "core.False.type")
+let build_coq_True () = pf_constr_of_global (lib_ref "core.True.type")
+let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I")
 
 let rec build_discriminator env sigma true_0 false_0 dirn c = function
   | [] ->
@@ -1320,15 +1325,15 @@ let inject_if_homogenous_dependent_pair ty =
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
-    let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
-    let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
+    let sigTconstr   = Coqlib.(lib_ref "core.sigT.type") in
+    let existTconstr = Coqlib.lib_ref    "core.sigT.intro" in
     (* check whether the equality deals with dep pairs or not *)
     let eqTypeDest = fst (decompose_app sigma t) in
-    if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit;
+    if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit;
     let hd1,ar1 = decompose_app_vect sigma t1 and
         hd2,ar2 = decompose_app_vect sigma t2 in
-    if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
-    if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
+    if not (Termops.is_global sigma existTconstr hd1) then raise Exit;
+    if not (Termops.is_global sigma existTconstr hd2) then raise Exit;
     let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
@@ -1336,17 +1341,16 @@ let inject_if_homogenous_dependent_pair ty =
     (* knows inductive types *)
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
-    Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
+    check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
-    let inj2 = Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"]
-                                    "inj_pair2_eq_dec" in
+    let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
        intro;
        onLastHyp (fun hyp ->
-        Tacticals.New.pf_constr_of_global Coqlib.glob_eq >>= fun ceq ->
+        Tacticals.New.pf_constr_of_global Coqlib.(lib_ref "core.eq.type") >>= fun ceq ->
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar sigma hyp];
            Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
@@ -1671,8 +1675,8 @@ let _ =
       optwrite = (:=) regular_subst_tactic }
 
 let restrict_to_eq_and_identity eq = (* compatibility *)
-  if not (is_global glob_eq eq) &&
-    not (is_global glob_identity eq) 
+  if not (is_global (lib_ref "core.eq.type") eq) &&
+    not (is_global (lib_ref "core.identity.type") eq)
   then raise Constr_matching.PatternMatchingFailure
 
 exception FoundHyp of (Id.t * constr * bool)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index af6d1c472f..245bdce5ad 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1292,13 +1292,13 @@ let project_hint ~poly pri l2r r =
   let sigma, c = Evd.fresh_global env sigma gr in
   let t = Retyping.get_type_of env sigma c in
   let t =
-    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+    Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t in
   let sign,ccl = decompose_prod_assum sigma t in
   let (a,b) = match snd (decompose_app sigma ccl) with
     | [a;b] -> (a,b)
     | _ -> assert false in
   let p =
-    if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+    if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
   let sigma, p = Evd.fresh_global env sigma p in
   let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a1bb0a7401..708412720a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -289,24 +289,22 @@ let coq_refl_jm_pattern       =
   mkPattern (mkGProd "A" mkGHole (mkGProd "x" (mkGVar "A")
     (mkGApp mkGHole [mkGVar "A"; mkGVar "x"; mkGVar "A"; mkGVar "x";])))
 
-open Globnames
-
 let match_with_equation env sigma t =
   if not (isApp sigma t) then raise NoEquationFound;
   let (hdapp,args) = destApp sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind,u) ->
-      if GlobRef.equal (IndRef ind) glob_eq then
-	Some (build_coq_eq_data()),hdapp,
-	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-      else if GlobRef.equal (IndRef ind) glob_identity then
-	Some (build_coq_identity_data()),hdapp,
-	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-      else if GlobRef.equal (IndRef ind) glob_jmeq then
-	Some (build_coq_jmeq_data()),hdapp,
-	HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
-      else
-        let (mib,mip) = Global.lookup_inductive ind in
+    if Coqlib.check_ind_ref "core.eq.type" ind then
+      Some (build_coq_eq_data()),hdapp,
+      PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+    else if Coqlib.check_ind_ref "core.identity.type" ind then
+      Some (build_coq_identity_data()),hdapp,
+      PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+    else if Coqlib.check_ind_ref "core.JMeq.type" ind then
+      Some (build_coq_jmeq_data()),hdapp,
+      HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+    else
+      let (mib,mip) = Global.lookup_inductive ind in
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 1 then
@@ -438,12 +436,12 @@ let match_eq sigma eqn (ref, hetero) =
   | _ -> raise PatternMatchingFailure
 
 let no_check () = true
-let check_jmeq_loaded () = Library.library_is_loaded @@ Coqlib.jmeq_library_path
+let check_jmeq_loaded () = has_ref "core.JMeq.type"
 
 let equalities =
-  [(coq_eq_ref, false), no_check, build_coq_eq_data;
-   (coq_jmeq_ref, true), check_jmeq_loaded, build_coq_jmeq_data;
-   (coq_identity_ref, false), no_check, build_coq_identity_data]
+  [(lazy(lib_ref "core.eq.type"), false), no_check, build_coq_eq_data;
+   (lazy(lib_ref "core.JMeq.type"), true), check_jmeq_loaded, build_coq_jmeq_data;
+   (lazy(lib_ref "core.identity.type"), false), no_check, build_coq_identity_data]
 
 let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
   let d,k = first_match (match_eq sigma eqn) equalities in
@@ -478,9 +476,9 @@ let find_this_eq_data_decompose gl eqn =
 
 let match_sigma env sigma ex =
   match EConstr.kind sigma ex with
-  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f -> 
+  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sig.intro") f ->
       build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
-  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_existT_ref) f -> 
+  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f ->
     build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
   | _ -> raise PatternMatchingFailure
     
@@ -489,7 +487,7 @@ let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *)
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern =
-  lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"]))
+  lazy (mkPattern (mkGAppRef (lazy (lib_ref "core.sig.type")) [mkGPatVar "X1"; mkGPatVar "X2"]))
 
 let match_sigma env sigma t =
   match Id.Map.bindings (matches env sigma (Lazy.force coq_sig_pattern) t) with
@@ -507,44 +505,44 @@ let is_matching_sigma env sigma t = is_matching env sigma (Lazy.force coq_sig_pa
 
 let coq_eqdec ~sum ~rev =
   lazy (
-    let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
-    let args = [eqn; mkGAppRef coq_not_ref [eqn]] in
+    let eqn = mkGAppRef (lazy (lib_ref "core.eq.type")) (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
+    let args = [eqn; mkGAppRef (lazy (lib_ref "core.not.type")) [eqn]] in
     let args = if rev then List.rev args else args in
     mkPattern (mkGAppRef sum args)
   )
 
+let sumbool_type = lazy (lib_ref "core.sumbool.type")
+let or_type = lazy (lib_ref "core.or.type")
+
 (** [{ ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 }] *)
-let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false
+let coq_eqdec_inf_pattern = coq_eqdec ~sum:sumbool_type ~rev:false
 
 (** [{ ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 }] *)
-let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true
+let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:sumbool_type ~rev:true
 
 (** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *)
-let coq_eqdec_pattern = coq_eqdec ~sum:coq_or_ref ~rev:false
+let coq_eqdec_pattern = coq_eqdec ~sum:or_type ~rev:false
 
 (** %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) *)
-let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true
-
-let op_or = coq_or_ref
-let op_sum = coq_sumbool_ref
+let coq_eqdec_rev_pattern = coq_eqdec ~sum:or_type ~rev:true
 
 let match_eqdec env sigma t =
   let eqonleft,op,subst =
-    try true,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t
+    try true,sumbool_type,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t
     with PatternMatchingFailure ->
-    try false,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
+    try false,sumbool_type,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
     with PatternMatchingFailure ->
-    try true,op_or,matches env sigma (Lazy.force coq_eqdec_pattern) t
+    try true,or_type,matches env sigma (Lazy.force coq_eqdec_pattern) t
     with PatternMatchingFailure ->
-        false,op_or,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in
+        false,or_type,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in
   match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
       eqonleft, Lazy.force op, c1, c2, typ
   | _ -> anomaly (Pp.str "Unexpected pattern.")
 
 (* Patterns "~ ?" and "? -> False" *)
-let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
-let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref)))
+let coq_not_pattern = lazy (mkPattern (mkGAppRef (lazy (lib_ref "core.not.type")) [mkGHole]))
+let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef (lazy (lib_ref "core.False.type")))))
 
 let is_matching_not env sigma t = is_matching env sigma (Lazy.force coq_not_pattern) t
 let is_matching_imp_False env sigma t = is_matching env sigma (Lazy.force coq_imp_False_pattern) t
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5ac4284b43..6a39a10fc4 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -350,7 +350,7 @@ let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter i
 let dest_nf_eq env sigma t = match EConstr.kind sigma t with
 | App (r, [| t; x; y |]) ->
   let open Reductionops in
-  let lazy eq = Coqlib.coq_eq_ref in
+  let eq = Coqlib.lib_ref "core.eq.type" in
   if EConstr.is_global sigma eq r then
     (t, whd_all env sigma x, whd_all env sigma y)
   else user_err Pp.(str "Not an equality.")
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3769dca6e0..9ec3e203cc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3552,12 +3552,13 @@ let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
   user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
-let coq_eq sigma       = Evarutil.new_global sigma (Coqlib.build_coq_eq ())
-let coq_eq_refl sigma  = Evarutil.new_global sigma (Coqlib.build_coq_eq_refl ())
+let coq_eq sigma       = Evarutil.new_global sigma Coqlib.(lib_ref "core.eq.type")
+let coq_eq_refl sigma  = Evarutil.new_global sigma Coqlib.(lib_ref "core.eq.refl")
 
-let coq_heq_ref        = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq_ref        = lazy (Coqlib.lib_ref "core.JMeq.type")
 let coq_heq sigma      = Evarutil.new_global sigma (Lazy.force coq_heq_ref)
-let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
+let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.JMeq.refl")
+(* let coq_heq_refl = lazy (glob (lib_ref "core.JMeq.refl")) *)
 
 let mkEq sigma t x y =
   let sigma, eq = coq_eq sigma in
@@ -3789,7 +3790,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
   let open Context.Named.Declaration in
   Proofview.Goal.enter begin fun gl ->
-  Coqlib.check_required_library Coqlib.jmeq_module_name;
+  Coqlib.(check_required_library jmeq_module_name);
   let sigma = Tacmach.New.project gl in
   let (f, args, def, id, oldid) =
     let oldid = Tacmach.New.pf_get_new_id id gl in
@@ -3849,7 +3850,7 @@ let specialize_eqs id =
     match EConstr.kind !evars ty with
     | Prod (na, t, b) ->
 	(match EConstr.kind !evars t with
-	| App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq ->
+        | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq ->
 	    let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
 	    let pt = mkApp (eq, [| eqty; c; c |]) in
             let ind = destInd !evars eq in