From 29919b725262dca76708192bde65ce82860747be Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 22:31:55 +0100
Subject: Granting #9516 and #9518 (support for numerals and strings in custom
 entries).

---
 interp/notation.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp/notation.mli')

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