From 68304575dd3fd85d26e2f1bdff84721df8481952 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 12 Oct 2018 12:22:43 +0000
Subject: [Numeral notations] Use Coqlib registered constants

---
 plugins/syntax/numeral.ml  | 34 +++++++++++++++++++++-------------
 theories/Init/Decimal.v    |  5 ++++-
 theories/Numbers/BinNums.v |  1 +
 3 files changed, 26 insertions(+), 14 deletions(-)

diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 470deb4a60..efd36ad03c 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -33,11 +33,12 @@ let get_constructors ind =
   Array.to_list
     (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
 
-let q_z = qualid_of_string "Coq.Numbers.BinNums.Z"
-let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive"
-let q_int = qualid_of_string "Coq.Init.Decimal.int"
-let q_uint = qualid_of_string "Coq.Init.Decimal.uint"
-let q_option = qualid_of_string "Coq.Init.Datatypes.option"
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_int () = qualid_of_ref "num.int.type"
+let q_uint () = qualid_of_ref "num.uint.type"
+let q_option () = qualid_of_ref "core.option.type"
 
 let unsafe_locate_ind q =
   match Nametab.locate q with
@@ -45,14 +46,22 @@ let unsafe_locate_ind q =
   | _ -> raise Not_found
 
 let locate_ind q =
+  let q = q () in
   try unsafe_locate_ind q
   with Not_found -> Nametab.error_global_not_found q
 
 let locate_z () =
-  try
-    Some { z_ty = unsafe_locate_ind q_z;
-           pos_ty = unsafe_locate_ind q_positive }
-  with Not_found -> None
+  let zn = "num.Z.type" in
+  let pn = "num.pos.type" in
+  if Coqlib.has_ref zn && Coqlib.has_ref pn
+  then
+    let q_z = qualid_of_ref zn in
+    let q_pos = qualid_of_ref pn in
+    Some ({
+        z_ty = unsafe_locate_ind q_z;
+        pos_ty = unsafe_locate_ind q_pos;
+    }, mkRefC q_z)
+  else None
 
 let locate_int () =
   { uint = locate_ind q_uint;
@@ -86,11 +95,10 @@ let vernac_numeral_notation local ty f g scope opts =
   let of_ty = Smartlocate.global_with_alias g in
   let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
-  let cref q = mkRefC q in
+  let cref q = mkRefC (q ()) in
   let arrow x y =
     mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
   in
-  let cZ = cref q_z in
   let cint = cref q_int in
   let cuint = cref q_uint in
   let coption = cref q_option in
@@ -104,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts =
     else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option
     else
       match z_pos_ty with
-      | Some z_pos_ty ->
+      | Some (z_pos_ty, cZ) ->
          if has_type f (arrow cZ cty) then Z z_pos_ty, Direct
          else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option
          else type_error_to f ty false
@@ -118,7 +126,7 @@ let vernac_numeral_notation local ty f g scope opts =
     else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option
     else
       match z_pos_ty with
-      | Some z_pos_ty ->
+      | Some (z_pos_ty, cZ) ->
          if has_type g (arrow cty cZ) then Z z_pos_ty, Direct
          else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option
          else type_error_of g ty false
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 537400fb05..3d4b3d0568 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -40,7 +40,7 @@ Notation zero := (D0 Nil).
 
 (** For signed integers, we use two constructors [Pos] and [Neg]. *)
 
-Inductive int := Pos (d:uint) | Neg (d:uint).
+Variant int := Pos (d:uint) | Neg (d:uint).
 
 Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
@@ -50,6 +50,9 @@ Declare Scope dec_int_scope.
 Delimit Scope dec_int_scope with int.
 Bind Scope dec_int_scope with int.
 
+Register uint as num.uint.type.
+Register int as num.int.type.
+
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
     and choose our canonical representation of 0 (here [D0 Nil]
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index ef2c688759..247827597a 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -29,6 +29,7 @@ Bind Scope positive_scope with positive.
 Arguments xO _%positive.
 Arguments xI _%positive.
 
+Register positive as num.pos.type.
 Register xI as num.pos.xI.
 Register xO as num.pos.xO.
 Register xH as num.pos.xH.
-- 
cgit v1.2.3