From 25cab58df1171c9419396342e9ecc3094b74eca5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Feb 2020 21:09:53 +0100
Subject: Revert "Granting #9516 and #9518 (support for numerals and strings in
 custom entries)."

This reverts commit 29919b725262dca76708192bde65ce82860747be.

It was pushed by mistake as part of #11530. Sorry about it.
---
 interp/notation.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 707be6cb87..ea5125f7ec 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -305,12 +305,9 @@ 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