diff options
| author | Hugo Herbelin | 2020-02-10 22:31:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-16 21:44:43 +0100 |
| commit | 29919b725262dca76708192bde65ce82860747be (patch) | |
| tree | 61694625fbeb3491bef8cb1f09f2a07548318acf /interp/notation.mli | |
| parent | acde8140bd51be112be33ae07db68b2f3b93302c (diff) | |
Granting #9516 and #9518 (support for numerals and strings in custom entries).
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index ea5125f7ec..707be6cb87 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -305,9 +305,12 @@ val availability_of_entry_coercion : notation_entry_level -> notation_entry_leve val declare_custom_entry_has_global : string -> int -> unit val declare_custom_entry_has_ident : string -> int -> unit +val declare_custom_entry_has_numeral : string -> int -> unit +val declare_custom_entry_has_string : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool +val entry_has_prim_token : prim_token -> notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) |