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

1 files changed, 5 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)