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

2 files changed, 24 insertions, 27 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index ba3fa6fa0d..e5b032e638 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -693,12 +693,7 @@ let rewrite_except h =
   end
 
 
-let refl_equal = 
-  let coq_base_constant s =
-    Coqlib.gen_reference_in_modules "RecursiveDefinition"
-      (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in
-  function () -> (coq_base_constant "eq_refl")
-
+let refl_equal () = Coqlib.lib_ref "core.eq.type"
 
 (* This is simply an implementation of the case_eq tactic.  this code
   should be replaced by a call to the tactic but I don't know how to
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5b8bd6d01a..9dd98a4ab7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -56,12 +56,14 @@ let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
   else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
 
+let find_reference dir s =
+  Coqlib.find_reference "generalized rewriting" dir s
+[@@warning "-3"]
+
 let lazy_find_reference dir s =
-  let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in
+  let gr = lazy (find_reference dir s) in
   fun () -> Lazy.force gr
 
-let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s
-
 type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 
 let find_global dir s =
@@ -74,13 +76,13 @@ let find_global dir s =
 
 (** Global constants. *)
 
-let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq"
-let coq_eq = find_global ["Init"; "Logic"] "eq"
-let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
-let coq_all = find_global ["Init"; "Logic"] "all"
-let impl = find_global ["Program"; "Basics"] "impl"
+let coq_eq_ref  () = Coqlib.lib_ref    "core.eq.type"
+let coq_eq      = find_global    ["Coq"; "Init"; "Logic"] "eq"
+let coq_f_equal = find_global    ["Coq"; "Init"; "Logic"] "f_equal"
+let coq_all     = find_global    ["Coq"; "Init"; "Logic"] "all"
+let impl        = find_global    ["Coq"; "Program"; "Basics"] "impl"
 
-(** Bookkeeping which evars are constraints so that we can 
+(** Bookkeeping which evars are constraints so that we can
     remove them at the end of the tactic. *)
 
 let goalevars evars = fst evars
@@ -154,7 +156,7 @@ end) = struct
   let respectful = find_global morphisms "respectful"
   let respectful_ref = lazy_find_reference morphisms "respectful"
 
-  let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation"
+  let default_relation = find_global ["Coq"; "Classes"; "SetoidTactics"] "DefaultRelation"
 
   let coq_forall = find_global morphisms "forall_def"
 
@@ -374,12 +376,12 @@ let type_app_poly env env evd f args =
 module PropGlobal = struct
   module Consts =
   struct 
-    let relation_classes = ["Classes"; "RelationClasses"]
-    let morphisms = ["Classes"; "Morphisms"]
-    let relation = ["Relations";"Relation_Definitions"], "relation"
+    let relation_classes = ["Coq"; "Classes"; "RelationClasses"]
+    let morphisms = ["Coq"; "Classes"; "Morphisms"]
+    let relation = ["Coq"; "Relations";"Relation_Definitions"], "relation"
     let app_poly = app_poly_nocheck
-    let arrow = find_global ["Program"; "Basics"] "arrow"
-    let coq_inverse = find_global ["Program"; "Basics"] "flip"
+    let arrow = find_global ["Coq"; "Program"; "Basics"] "arrow"
+    let coq_inverse = find_global ["Coq"; "Program"; "Basics"] "flip"
   end
 
   module G = GlobalBindings(Consts)
@@ -395,12 +397,12 @@ end
 module TypeGlobal = struct
   module Consts = 
     struct 
-      let relation_classes = ["Classes"; "CRelationClasses"]
-      let morphisms = ["Classes"; "CMorphisms"]
+      let relation_classes = ["Coq"; "Classes"; "CRelationClasses"]
+      let morphisms = ["Coq"; "Classes"; "CMorphisms"]
       let relation = relation_classes, "crelation"
       let app_poly = app_poly_check
-      let arrow = find_global ["Classes"; "CRelationClasses"] "arrow"
-      let coq_inverse = find_global ["Classes"; "CRelationClasses"] "flip"
+      let arrow = find_global ["Coq"; "Classes"; "CRelationClasses"] "arrow"
+      let coq_inverse = find_global ["Coq"; "Classes"; "CRelationClasses"] "flip"
     end
 
   module G = GlobalBindings(Consts)
@@ -740,9 +742,9 @@ let new_global (evars, cstrs) gr =
   (sigma, cstrs), c
 
 let make_eq sigma =
-  new_global sigma (Coqlib.build_coq_eq ())
+  new_global sigma Coqlib.(lib_ref "core.eq.type")
 let make_eq_refl sigma =
-  new_global sigma (Coqlib.build_coq_eq_refl ())
+  new_global sigma Coqlib.(lib_ref "core.eq.refl")
 
 let get_rew_prf evars r = match r.rew_prf with
   | RewPrf (rel, prf) -> evars, (rel, prf)