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/constrextern.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'interp/constrextern.ml')

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)
-- 
cgit v1.2.3