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

3 files changed, 57 insertions, 43 deletions

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 600e8993b4..99c02995fb 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -319,6 +319,9 @@ Arguments F_empty [A].
 Arguments F_push [A] a S _.
 Arguments In [A] x S F.
 
+Register empty as plugins.rtauto.empty.
+Register push as plugins.rtauto.push.
+
 Section Map.
 
 Variables A B:Set.
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index 06cdf76b4e..f027a4a46e 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -387,3 +387,24 @@ exact (Reflect (empty \ A \ B \ C)
 Qed.
 Print toto.
 *)
+
+Register Reflect as plugins.rtauto.Reflect.
+
+Register Atom as plugins.rtauto.Atom.
+Register Arrow as plugins.rtauto.Arrow.
+Register Bot as plugins.rtauto.Bot.
+Register Conjunct as plugins.rtauto.Conjunct.
+Register Disjunct as plugins.rtauto.Disjunct.
+
+Register Ax as plugins.rtauto.Ax.
+Register I_Arrow as plugins.rtauto.I_Arrow.
+Register E_Arrow as plugins.rtauto.E_Arrow.
+Register D_Arrow as plugins.rtauto.D_Arrow.
+Register E_False as plugins.rtauto.E_False.
+Register I_And as plugins.rtauto.I_And.
+Register E_And as plugins.rtauto.E_And.
+Register D_And as plugins.rtauto.D_And.
+Register I_Or_l as plugins.rtauto.I_Or_l.
+Register I_Or_r as plugins.rtauto.I_Or_r.
+Register E_Or as plugins.rtauto.E_Or.
+Register D_Or as plugins.rtauto.D_Or.
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 8a0f48dc4d..79418da27c 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -26,49 +26,39 @@ let step_count = ref 0
 
 let node_count = ref 0
 
-let logic_constant s = UnivGen.constr_of_global @@
-  Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s
-
-let li_False = lazy (destInd (logic_constant "False"))
-let li_and   = lazy (destInd (logic_constant "and"))
-let li_or    = lazy (destInd (logic_constant "or"))
-
-let pos_constant s = UnivGen.constr_of_global @@
-  Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s
-
-let l_xI = lazy (pos_constant "xI")
-let l_xO = lazy (pos_constant "xO")
-let l_xH = lazy (pos_constant "xH")
-
-let store_constant s = UnivGen.constr_of_global @@
-  Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s
-
-let l_empty = lazy (store_constant "empty")
-let l_push = lazy (store_constant "push")
-
-let constant s = UnivGen.constr_of_global @@
-  Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s
-
-let l_Reflect = lazy (constant "Reflect")
-
-let l_Atom = lazy (constant "Atom")
-let l_Arrow = lazy (constant "Arrow")
-let l_Bot = lazy (constant "Bot")
-let l_Conjunct = lazy (constant "Conjunct")
-let l_Disjunct = lazy (constant "Disjunct")
-
-let l_Ax = lazy (constant "Ax")
-let l_I_Arrow = lazy (constant "I_Arrow")
-let l_E_Arrow = lazy (constant "E_Arrow")
-let l_D_Arrow = lazy (constant "D_Arrow")
-let l_E_False = lazy (constant "E_False")
-let l_I_And = lazy (constant "I_And")
-let l_E_And = lazy (constant "E_And")
-let l_D_And = lazy (constant "D_And")
-let l_I_Or_l = lazy (constant "I_Or_l")
-let l_I_Or_r = lazy (constant "I_Or_r")
-let l_E_Or = lazy (constant "E_Or")
-let l_D_Or = lazy (constant "D_Or")
+let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type"))
+let li_and   = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type"))
+let li_or    = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type"))
+
+let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n))
+
+let l_xI = gen_constant "num.pos.xI"
+let l_xO = gen_constant "num.pos.xO"
+let l_xH = gen_constant "num.pos.xH"
+
+let l_empty = gen_constant "plugins.rtauto.empty"
+let l_push = gen_constant "plugins.rtauto.push"
+
+let l_Reflect = gen_constant "plugins.rtauto.Reflect"
+
+let l_Atom = gen_constant "plugins.rtauto.Atom"
+let l_Arrow = gen_constant "plugins.rtauto.Arrow"
+let l_Bot = gen_constant "plugins.rtauto.Bot"
+let l_Conjunct = gen_constant "plugins.rtauto.Conjunct"
+let l_Disjunct = gen_constant "plugins.rtauto.Disjunct"
+
+let l_Ax = gen_constant "plugins.rtauto.Ax"
+let l_I_Arrow = gen_constant "plugins.rtauto.I_Arrow"
+let l_E_Arrow = gen_constant "plugins.rtauto.E_Arrow"
+let l_D_Arrow = gen_constant "plugins.rtauto.D_Arrow"
+let l_E_False = gen_constant "plugins.rtauto.E_False"
+let l_I_And = gen_constant "plugins.rtauto.I_And"
+let l_E_And = gen_constant "plugins.rtauto.E_And"
+let l_D_And = gen_constant "plugins.rtauto.D_And"
+let l_I_Or_l = gen_constant "plugins.rtauto.I_Or_l"
+let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r"
+let l_E_Or = gen_constant "plugins.rtauto.E_Or"
+let l_D_Or = gen_constant "plugins.rtauto.D_Or"
 
 
 let special_whd gl c =