1 files changed, 42 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli
index 6e59c0fd70..734198bbf6 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -102,10 +102,51 @@ val register_bignumeral_interpretation :
 val register_string_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
 
+(** * Numeral notation *)
+
+type numeral_notation_error =
+  | UnexpectedTerm of Constr.t
+  | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
+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_interp_info =
+    Uid of prim_token_uid
+  | NumeralNotation of numeral_notation_obj
+
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
-  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
   pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)