Merge PR #11636: Revert buggy commit mistakenly pushed with #11530

Reviewed-by: ejgallego

3 files changed, 3 insertions, 36 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 06232b8e1a..c198c4eb9b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -792,11 +792,9 @@ let rec flatten_application c = match DAst.get c with
 
 let extern_possible_prim_token (custom,scopes) r =
    let (sc,n) = uninterp_prim_token r in
-   let coercion =
-     if entry_has_prim_token n custom then [] else
-     match availability_of_entry_coercion custom InConstrEntrySomeLevel with
-     | None -> raise No_match
-     | Some coercion -> coercion in
+   match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+   | None -> raise No_match
+   | Some coercion ->
    match availability_of_prim_token n sc scopes with
    | None -> raise No_match
    | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
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
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 *)