Fix Numeral Notations (1/4 - moving things)

Move various things from from numeral.ml to notation.ml and
notation.mli; this is required to allow the vernac command to continue
living in numeral.ml while preparing to move all of the numeral notation
interpretation logic to notation.ml

This is commit 1/4 in the fix for #8401.

This is a pure cut/paste commit, modulo adding section-heading comments.

5 files changed, 65 insertions, 35 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index a6a14efc87..8cb423051a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -387,6 +387,37 @@ let prim_token_interpreters =
 let prim_token_uninterpreters =
   (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
 
+(*******************************************************)
+(* Numeral notation interpretation                     *)
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+type int_ty =
+  { uint : Names.inductive;
+    int : Names.inductive }
+
+type z_pos_ty =
+  { z_ty : Names.inductive;
+    pos_ty : Names.inductive }
+
+type target_kind =
+  | Int of int_ty (* Coq.Init.Decimal.int + uint *)
+  | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+  | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+type numeral_notation_obj =
+  { to_kind : conversion_kind;
+    to_ty : GlobRef.t;
+    of_kind : conversion_kind;
+    of_ty : GlobRef.t;
+    num_ty : Libnames.qualid; (* for warnings / error messages *)
+    warning : numnot_option }
+
 (* Table from scope_name to backtrack-able informations about interpreters
    (in particular interpreter unique id). *)
 let prim_token_interp_infos =
diff --git a/interp/notation.mli b/interp/notation.mli
index 6e59c0fd70..7f20a2ef1f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -102,6 +102,37 @@ val register_bignumeral_interpretation :
 val register_string_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
 
+(** * Numeral notation *)
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+type int_ty =
+  { uint : Names.inductive;
+    int : Names.inductive }
+
+type z_pos_ty =
+  { z_ty : Names.inductive;
+    pos_ty : Names.inductive }
+
+type target_kind =
+  | Int of int_ty (* Coq.Init.Decimal.int + uint *)
+  | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+  | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+type numeral_notation_obj =
+  { to_kind : conversion_kind;
+    to_ty : GlobRef.t;
+    of_kind : conversion_kind;
+    of_ty : GlobRef.t;
+    num_ty : Libnames.qualid; (* for warnings / error messages *)
+    warning : numnot_option }
+
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index ec14df3baa..55f61a58f9 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
+open Notation
 open Numeral
 open Pp
 open Names
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index fee93593d0..7acf18da2f 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -16,6 +16,7 @@ open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Constr
+open Notation
 
 (** * Numeral notation *)
 
@@ -96,10 +97,6 @@ let rec rawnum_compare s s' =
 
 (** ** Conversion between Coq [Decimal.int] and internal raw string *)
 
-type int_ty =
-  { uint : Names.inductive;
-    int : Names.inductive }
-
 (** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
 
 let digit_of_char c =
@@ -158,10 +155,6 @@ let rawnum_of_coqint c =
 
 (** ** Conversion between Coq [Z] and internal bigint *)
 
-type z_pos_ty =
-  { z_ty : Names.inductive;
-    pos_ty : Names.inductive }
-
 (** First, [positive] from/to bigint *)
 
 let rec pos_of_bigint posty n =
@@ -273,27 +266,6 @@ let big2raw n =
 let raw2big (n,s) =
   if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
 
-type target_kind =
-  | Int of int_ty (* Coq.Init.Decimal.int + uint *)
-  | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
-  | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
-
-type option_kind = Option | Direct
-type conversion_kind = target_kind * option_kind
-
-type numnot_option =
-  | Nop
-  | Warning of raw_natural_number
-  | Abstract of raw_natural_number
-
-type numeral_notation_obj =
-  { to_kind : conversion_kind;
-    to_ty : GlobRef.t;
-    of_kind : conversion_kind;
-    of_ty : GlobRef.t;
-    num_ty : Libnames.qualid; (* for warnings / error messages *)
-    warning : numnot_option }
-
 let interp o ?loc n =
   begin match o.warning with
   | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 83ede6f48f..f96b8321f8 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -9,14 +9,9 @@
 (************************************************************************)
 
 open Libnames
-open Constrexpr
 open Vernacexpr
+open Notation
 
 (** * Numeral notation *)
 
-type numnot_option =
-  | Nop
-  | Warning of raw_natural_number
-  | Abstract of raw_natural_number
-
 val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit