diff options
| author | Jason Gross | 2018-11-27 21:03:57 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:01:17 -0500 |
| commit | f7992de2dc4ce0091197b9476779fc120a2fd9ec (patch) | |
| tree | 236d3a9e0b2e357b893653d97b41303cb8d5529c /interp/notation.mli | |
| parent | 26ef08ab681661c03c8bffa88d7bec949d692f58 (diff) | |
Factor out common code in numeral/string notations
As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 28 |
1 files changed, 11 insertions, 17 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 6880b9a2cd..c0ff1a1ac3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -104,12 +104,11 @@ val register_string_interpretation : (** * Numeral notation *) -type numeral_or_string_notation_error = +type prim_token_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error -exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error +exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error type numnot_option = | Nop @@ -134,23 +133,18 @@ type string_target_kind = | Byte type option_kind = Option | Direct -type conversion_kind = target_kind * option_kind -type string_conversion_kind = string_target_kind * option_kind +type 'target conversion_kind = 'target * option_kind -type numeral_notation_obj = - { to_kind : conversion_kind; +type ('target, 'warning) prim_token_notation_obj = + { to_kind : 'target conversion_kind; to_ty : GlobRef.t; - of_kind : conversion_kind; + of_kind : 'target conversion_kind; of_ty : GlobRef.t; - num_ty : Libnames.qualid; (* for warnings / error messages *) - warning : numnot_option } - -type string_notation_obj = - { sto_kind : string_conversion_kind; - sto_ty : GlobRef.t; - sof_kind : string_conversion_kind; - sof_ty : GlobRef.t; - string_ty : Libnames.qualid (* for warnings / error messages *) } + ty_name : Libnames.qualid; (* for warnings / error messages *) + warning : 'warning } + +type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj +type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj type prim_token_interp_info = Uid of prim_token_uid |