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.

11 files changed, 9 insertions, 67 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 *)
 
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 178f7354f2..848861238a 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -29,7 +29,6 @@ type 'a constr_entry_key_gen =
   | ETIdent
   | ETGlobal
   | ETBigint
-  | ETString
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
@@ -54,7 +53,6 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
-  | ETProdString          (* Parsed as a string *)
   | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
   | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5c220abeda..a5ade43295 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -55,12 +55,11 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | ETIdent, ETIdent -> true
 | ETGlobal, ETGlobal -> true
 | ETBigint, ETBigint -> true
-| ETString, ETString -> true
 | ETBinder b1, ETBinder b2 -> b1 == b2
 | ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
    notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
+| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
 let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 1c8f237bb8..807914a671 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -14,8 +14,6 @@ Entry constr:myconstr is
      : nat
 [<< # 0 >>]
      : option nat
-[2 + 3]
-     : nat
 [1 {f 1}]
      : Expr
 fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4ab800c9ba..2906698386 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -22,9 +22,6 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a
 Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
 Check [ << # 0 >> ].
 
-Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
-Check [ 2 + 3 ].
-
 End A.
 
 Module B.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 5e98f5ddc0..3181bcc4bc 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -249,7 +249,6 @@ type (_, _) entry =
 | TTName : ('self, lname) entry
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, string) entry
-| TTString : ('self, string) entry
 | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -370,14 +369,12 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTName -> MayRecNo (Aentry Prim.name)
 | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
 | TTBigint -> MayRecNo (Aentry Prim.bigint)
-| TTString -> MayRecNo (Aentry Prim.string)
 | TTReference -> MayRecNo (Aentry Constr.global)
 
 let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
-| ETProdString -> TTAny TTString
 | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
 | ETProdPattern p -> TTAny (TTPattern p)
 | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
@@ -417,11 +414,6 @@ match e with
   | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v)))
   | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v)))
   end
-| TTString ->
-  begin match forpat with
-  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (String v))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v))
-  end
 | TTReference ->
   begin match forpat with
   | ForConstr  -> push_constr subst (CAst.make @@ CRef (v, None))
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 97c9d23c68..28b9fa7449 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1234,7 +1234,6 @@ GRAMMAR EXTEND Gram
   syntax_extension_type:
     [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
-      | IDENT "string" -> { ETString }
       | IDENT "binder" -> { ETBinder true }
       | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
       | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index d39ee60c25..7794b0a37a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -396,7 +396,7 @@ let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
   let prec = unparsing_precedence_of_entry_type from x in
   match x with
-  | ETConstr _ | ETGlobal | ETBigint | ETString ->
+  | ETConstr _ | ETGlobal | ETBigint ->
      UnpMetaVar (i,prec)
   | ETPattern _ ->
      UnpBinderMetaVar (i,prec)
@@ -686,7 +686,6 @@ let prod_entry_type = function
   | ETIdent -> ETProdName
   | ETGlobal -> ETProdReference
   | ETBigint -> ETProdBigint
-  | ETString -> ETProdString
   | ETBinder _ -> assert false (* See check_binder_type *)
   | ETConstr (s,_,p) -> ETProdConstr (s,p)
   | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
@@ -990,7 +989,7 @@ let set_entry_type from n etyps (x,typ) =
       | ETConstr (s,bko,n), InternalProd ->
           ETConstr (s,bko,(n,InternalProd))
       | ETPattern (b,n), _ -> ETPattern (b,n)
-      | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x
+      | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
     with Not_found ->
       ETConstr (from,None,(make_lev n from,typ))
   in (x,typ)
@@ -1012,7 +1011,7 @@ let join_auxiliary_recursive_types recvars etyps =
 
 let internalization_type_of_entry_type = function
   | ETBinder _ -> NtnInternTypeOnlyBinder
-  | ETConstr _ | ETBigint | ETString | ETGlobal
+  | ETConstr _ | ETBigint | ETGlobal
   | ETIdent | ETPattern _ -> NtnInternTypeAny
 
 let set_internalization_type typs =
@@ -1034,7 +1033,7 @@ let make_interpretation_type isrec isonlybinding = function
   (* Others *)
   | ETIdent -> NtnTypeBinder NtnParsedAsIdent
   | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
-  | ETBigint | ETString | ETGlobal -> NtnTypeConstr
+  | ETBigint | ETGlobal -> NtnTypeConstr
   | ETBinder _ ->
      if isrec then NtnTypeBinderList
      else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
@@ -1098,8 +1097,6 @@ type entry_coercion_kind =
   | IsEntryCoercion of notation_entry_level
   | IsEntryGlobal of string * int
   | IsEntryIdent of string * int
-  | IsEntryNumeral of string * int
-  | IsEntryString of string * int
 
 let is_coercion = function
   | Some (custom,n,_,[e]) ->
@@ -1111,8 +1108,6 @@ let is_coercion = function
          else Some (IsEntryCoercion subentry)
      | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
      | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
-     | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n))
-     | ETString, InCustomEntry s -> Some (IsEntryString (s,n))
      | _ -> None)
   | Some _ -> assert false
   | None -> None
@@ -1154,7 +1149,7 @@ let find_precedence custom lev etyps symbols onlyprint =
           user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
       (try match List.assoc x etyps, custom with
         | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
-        | (ETIdent | ETBigint | ETString | ETGlobal), _ ->
+        | (ETIdent | ETBigint | ETGlobal), _ ->
             begin match lev with
             | None ->
               ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1380,8 +1375,6 @@ let open_notation i (_, nobj) =
     | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
     | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
     | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
-    | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n
-    | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n
     | None -> ())
   end
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0cf407619b..f4918caeff 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -126,7 +126,6 @@ open Pputils
     | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
     | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
     | ETBigint -> str "bigint"
-    | ETString -> str "string"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"