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

1 files changed, 13 insertions, 0 deletions

diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index 7b6740e94b..ef2c688759 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -29,6 +29,10 @@ Bind Scope positive_scope with positive.
 Arguments xO _%positive.
 Arguments xI _%positive.
 
+Register xI as num.pos.xI.
+Register xO as num.pos.xO.
+Register xH as num.pos.xH.
+
 (** [N] is a datatype representing natural numbers in a binary way,
     by extending the [positive] datatype with a zero.
     Numbers in [N] will also be denoted using a decimal notation;
@@ -43,6 +47,10 @@ Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
 Arguments Npos _%positive.
 
+Register N as num.N.type.
+Register N0 as num.N.N0.
+Register Npos as num.N.Npos.
+
 (** [Z] is a datatype representing the integers in a binary way.
     An integer is either zero or a strictly positive number
     (coded as a [positive]) or a strictly negative number
@@ -60,3 +68,8 @@ Delimit Scope Z_scope with Z.
 Bind Scope Z_scope with Z.
 Arguments Zpos _%positive.
 Arguments Zneg _%positive.
+
+Register Z as num.Z.type.
+Register Z0 as num.Z.Z0.
+Register Zpos as num.Z.Zpos.
+Register Zneg as num.Z.Zneg.