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.
---
 interp/notation.mli | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

(limited to 'interp/notation.mli')

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