From e39c84ff2dc20ce059ee6198e142ca076de8c6cb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Sep 2018 09:22:12 -0400
Subject: 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.
---
 plugins/syntax/g_numeral.ml4 |  1 +
 plugins/syntax/numeral.ml    | 30 +-----------------------------
 plugins/syntax/numeral.mli   |  7 +------
 3 files changed, 3 insertions(+), 35 deletions(-)

(limited to 'plugins/syntax')

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
-- 
cgit v1.2.3