diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 33e275d925..76bf70d452 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -139,6 +139,11 @@ type numeral_notation_obj = num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } +module Numeral : sig + val interp : numeral_notation_obj -> rawnum prim_token_interpreter + val uninterp : numeral_notation_obj -> rawnum prim_token_uninterpreter +end + type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) pt_scope : scope_name; (** Concerned scope *) |