diff options
| author | Hugo Herbelin | 2020-02-19 21:09:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-19 21:09:53 +0100 |
| commit | 25cab58df1171c9419396342e9ecc3094b74eca5 (patch) | |
| tree | 3bca55801e7915c333af55a5f876a869499d7d70 /interp/constrextern.ml | |
| parent | 43c3c7d6f62a9bee4772242c27fbafd54770d271 (diff) | |
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.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 8 |
1 files changed, 3 insertions, 5 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) |