From 8ac6145d5cc14823df48698a755d8adf048f026c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2017 12:22:32 +0200 Subject: [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 Co-authored-by: Maxime Dénès Co-authored-by: Vincent Laporte --- theories/Numbers/BinNums.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'theories/Numbers') 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. -- cgit v1.2.3