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.ml | 28 ----------------------------
 1 file changed, 28 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 9d6cab550d..93969f3718 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1349,34 +1349,6 @@ let entry_has_ident = function
   | InCustomEntryLevel (s,n) ->
      try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
 
-let entry_has_numeral_map = ref String.Map.empty
-let entry_has_string_map = ref String.Map.empty
-
-let declare_custom_entry_has_numeral s n =
-  try
-    let p = String.Map.find s !entry_has_numeral_map in
-    user_err (str "Custom entry " ++ str s ++
-              str " has already a rule for numerals at level " ++ int p ++ str ".")
-  with Not_found ->
-    entry_has_numeral_map := String.Map.add s n !entry_has_numeral_map
-
-let declare_custom_entry_has_string s n =
-  try
-    let p = String.Map.find s !entry_has_string_map in
-    user_err (str "Custom entry " ++ str s ++
-              str " has already a rule for strings at level " ++ int p ++ str ".")
-  with Not_found ->
-    entry_has_string_map := String.Map.add s n !entry_has_string_map
-
-let entry_has_prim_token prim = function
-  | InConstrEntrySomeLevel -> true
-  | InCustomEntryLevel (s,n) ->
-     match prim with
-     | Numeral _ ->
-       (try String.Map.find s !entry_has_numeral_map <= n with Not_found -> false)
-     | String _ ->
-       (try String.Map.find s !entry_has_string_map <= n with Not_found -> false)
-
 let uninterp_prim_token c =
   match glob_prim_constr_key c with
   | None -> raise Notation_ops.No_match
-- 
cgit v1.2.3