Granting #9516 and #9518 (support for numerals and strings in custom entries).

3 files changed, 36 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c198c4eb9b..06232b8e1a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -792,9 +792,11 @@ 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
-   match availability_of_entry_coercion custom InConstrEntrySomeLevel with
-   | None -> raise No_match
-   | Some coercion ->
+   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_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 93969f3718..9d6cab550d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1349,6 +1349,34 @@ 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 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 *)