Providing an API to access the parsing engine summary in a first-class way.

Instead of hardwiring a few special cases in Egramcoq, we allow the grammar
state to contain arbitrary data structures. This permits to extend the parsing
engine while retaining the synchronization with the global state, e.g. for use
in plugins.

9 files changed, 283 insertions, 267 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index f9f3ee988e..adfbd8cfde 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -140,7 +140,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
      <:str_item< do {
       Pptactic.declare_extra_genarg_pprule
         $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$;
-      Egramcoq.create_ltac_quotation $se$
+      Tacentries.create_ltac_quotation $se$
         (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v))
         ($lid:s$, None)
       } >> ]
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index d33ec91f9d..4d3507cbc4 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -25,7 +25,7 @@ open Locus
 
 let create_generic_quotation name e wit =
   let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
-  Egramcoq.create_ltac_quotation name inject (e, None)
+  Tacentries.create_ltac_quotation name inject (e, None)
 
 let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
 let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
@@ -38,7 +38,7 @@ let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Con
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
-  Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+  Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
 
 (* Rewriting orientation *)
 
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 711cd8d9d0..99c2213e19 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Libobject
+open Genarg
 open Pcoq
 open Egramml
 open Egramcoq
@@ -19,6 +20,196 @@ open Libnames
 open Nameops
 
 (**********************************************************************)
+(* Interpret entry names of the form "ne_constr_list" as entry keys   *)
+
+let coincide s pat off =
+  let len = String.length pat in
+  let break = ref true in
+  let i = ref 0 in
+  while !break && !i < len do
+    let c = Char.code s.[off + !i] in
+    let d = Char.code pat.[!i] in
+    break := Int.equal c d;
+    incr i
+  done;
+  !break
+
+let atactic n =
+  let open Extend in
+  if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
+  else Aentryl (name_of_entry Tactic.tactic_expr, n)
+
+type entry_name = EntryName :
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
+
+let try_get_entry u s =
+  let open Extend in
+  (** Order the effects: get_entry can raise Not_found *)
+  let TypedEntry (typ, e) = get_entry u s in
+  EntryName (typ, Aentry (name_of_entry e))
+
+(** Quite ad-hoc *)
+let get_tacentry n m =
+  let open Extend in
+  let check_lvl n =
+    Int.equal m n
+    && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
+    && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
+  in
+  if check_lvl n then EntryName (rawwit Constrarg.wit_tactic, Aself)
+  else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext)
+  else EntryName (rawwit Constrarg.wit_tactic, atactic n)
+
+let rec parse_user_entry s sep =
+  let open Extend in
+  let l = String.length s in
+  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
+    let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+    Ulist1 entry
+  else if l > 12 && coincide s "ne_" 0 &&
+                   coincide s "_list_sep" (l-9) then
+    let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
+    Ulist1sep (entry, sep)
+  else if l > 5 && coincide s "_list" (l-5) then
+    let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+    Ulist0 entry
+  else if l > 9 && coincide s "_list_sep" (l-9) then
+    let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
+    Ulist0sep (entry, sep)
+  else if l > 4 && coincide s "_opt" (l-4) then
+    let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+    Uopt entry
+  else if l > 5 && coincide s "_mods" (l-5) then
+    let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
+    Umodifiers entry
+  else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
+    let n = Char.code s.[6] - 48 in
+    Uentryl ("tactic", n)
+  else
+    let s = match s with "hyp" -> "var" | _ -> s in
+    Uentry s
+
+let arg_list = function Rawwit t -> Rawwit (ListArg t)
+let arg_opt = function Rawwit t -> Rawwit (OptArg t)
+
+let interp_entry_name up_level s sep =
+  let open Extend in
+  let rec eval = function
+  | Ulist1 e ->
+    let EntryName (t, g) = eval e in
+    EntryName (arg_list t, Alist1 g)
+  | Ulist1sep (e, sep) ->
+    let EntryName (t, g) = eval e in
+    EntryName (arg_list t, Alist1sep (g, sep))
+  | Ulist0 e ->
+    let EntryName (t, g) = eval e in
+    EntryName (arg_list t, Alist0 g)
+  | Ulist0sep (e, sep) ->
+    let EntryName (t, g) = eval e in
+    EntryName (arg_list t, Alist0sep (g, sep))
+  | Uopt e ->
+    let EntryName (t, g) = eval e in
+    EntryName (arg_opt t, Aopt g)
+  | Umodifiers e ->
+    let EntryName (t, g) = eval e in
+    EntryName (arg_list t, Amodifiers g)
+  | Uentry s ->
+    begin
+      try try_get_entry uprim s with Not_found ->
+      try try_get_entry uconstr s with Not_found ->
+      try try_get_entry utactic s with Not_found ->
+      error ("Unknown entry "^s^".")
+    end
+  | Uentryl (s, n) ->
+    (** FIXME: do better someday *)
+    assert (String.equal s "tactic");
+    get_tacentry n up_level
+  in
+  eval (parse_user_entry s sep)
+
+(**********************************************************************)
+(** Grammar declaration for Tactic Notation (Coq level)               *)
+
+let get_tactic_entry n =
+  if Int.equal n 0 then
+    Tactic.simple_tactic, None
+  else if Int.equal n 5 then
+    Tactic.binder_tactic, None
+  else if 1<=n && n<5 then
+    Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
+  else
+    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+
+(**********************************************************************)
+(** State of the grammar extensions                                   *)
+
+type tactic_grammar = {
+  tacgram_level : int;
+  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
+}
+
+(** ML Tactic grammar extensions *)
+
+let add_ml_tactic_entry (name, prods) =
+  let entry = Tactic.simple_tactic in
+  let mkact i loc l : Tacexpr.raw_tactic_expr =
+    let open Tacexpr in
+    let entry = { mltac_name = name; mltac_index = i } in
+    let map arg = TacGeneric arg in
+    TacML (loc, entry, List.map map l)
+  in
+  let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
+  synchronize_level_positions ();
+  grammar_extend entry None (None, [(None, None, List.rev rules)]);
+  1
+
+(* Declaration of the tactic grammar rule *)
+
+let head_is_ident tg = match tg.tacgram_prods with
+| GramTerminal _::_ -> true
+| _ -> false
+
+(** Tactic grammar extensions *)
+
+let add_tactic_entry (kn, tg) =
+  let open Tacexpr in
+  let entry, pos = get_tactic_entry tg.tacgram_level in
+  let mkact loc l =
+    let filter = function
+    | GramTerminal _ -> None
+    | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t)
+    in
+    let types = List.map_filter filter tg.tacgram_prods in
+    let map arg t =
+      (** HACK to handle especially the tactic(...) entry *)
+      let wit = Genarg.rawwit Constrarg.wit_tactic in
+      if Genarg.argument_type_eq t (Genarg.unquote wit) then
+        Tacexp (Genarg.out_gen wit arg)
+      else
+        TacGeneric arg
+    in
+    let l = List.map2 map l types in
+    (TacAlias (loc,kn,l):raw_tactic_expr)
+  in
+  let () =
+    if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
+      error "Notation for simple tactic must start with an identifier."
+  in
+  let rules = make_rule mkact tg.tacgram_prods in
+  synchronize_level_positions ();
+  grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
+  1
+
+let tactic_grammar =
+  create_grammar_command "TacticGrammar" add_tactic_entry
+
+let ml_tactic_grammar =
+  create_grammar_command "MLTacticGrammar" add_ml_tactic_entry
+
+let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn)
+let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
+
+(**********************************************************************)
 (* Tactic Notation                                                    *)
 
 let interp_prod_item lev = function
@@ -63,13 +254,13 @@ let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
   let () = check_key key in
   Tacenv.register_alias key tobj.tacobj_body;
-  Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
+  extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
 
 let open_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
   if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+    extend_tactic_grammar key tobj.tacobj_tacgram
 
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
@@ -78,7 +269,7 @@ let load_tactic_notation i (_, tobj) =
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
   if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+    extend_tactic_grammar key tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
   let (ids, body) = tobj.tacobj_body in
@@ -188,6 +379,37 @@ let add_ml_tactic_notation name prods =
   Lib.add_anonymous_leaf (inMLTacticGrammar obj);
   extend_atomic_tactic name prods
 
+(**********************************************************************)
+(** Ltac quotations                                                   *)
+
+let ltac_quotations = ref String.Set.empty
+
+let create_ltac_quotation name cast (e, l) =
+  let open Extend in
+  let () =
+    if String.Set.mem name !ltac_quotations then
+      failwith ("Ltac quotation " ^ name ^ " already registered")
+  in
+  let () = ltac_quotations := String.Set.add name !ltac_quotations in
+  let entry = match l with
+  | None -> Aentry (name_of_entry e)
+  | Some l -> Aentryl (name_of_entry e, l)
+  in
+(*   let level = Some "1" in *)
+  let level = None in
+  let assoc = None in
+  let rule =
+    Next (Next (Next (Next (Next (Stop,
+      Atoken (Lexer.terminal name)),
+      Atoken (Lexer.terminal ":")),
+      Atoken (Lexer.terminal "(")),
+      entry),
+      Atoken (Lexer.terminal ")"))
+  in
+  let action _ v _ _ _ loc = cast (loc, v) in
+  let gram = (level, assoc, [Rule (rule, action)]) in
+  Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
+
 (** Command *)
 
 
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 3cf0bc5cc9..b60d8f478e 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -19,3 +19,11 @@ val add_ml_tactic_notation : ml_tactic_name ->
   Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
 
 val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit
+
+(** {5 Adding tactic quotations} *)
+
+val create_ltac_quotation : string ->
+  ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
+(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
+    Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
+    generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 8c4930806e..f0c12ab8ef 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -217,115 +217,48 @@ let extend_constr_pat_notation ng =
   let ext = ETConstr (level, ()), ng.notgram_assoc in
   extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
 
-let extend_constr_notation ng =
+let extend_constr_notation (_, ng) =
   (* Add the notation in constr *)
   let nb = extend_constr_constr_notation ng in
   (* Add the notation in cases_pattern *)
   let nb' = extend_constr_pat_notation ng in
   nb + nb'
 
-(**********************************************************************)
-(** Grammar declaration for Tactic Notation (Coq level)               *)
-
-let get_tactic_entry n =
-  if Int.equal n 0 then
-    Tactic.simple_tactic, None
-  else if Int.equal n 5 then
-    Tactic.binder_tactic, None
-  else if 1<=n && n<5 then
-    Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
-  else
-    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+module GrammarCommand = Dyn.Make(struct end)
+module GrammarInterp = struct type 'a t = 'a -> int end
+module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
 
-(**********************************************************************)
-(** State of the grammar extensions                                   *)
+let grammar_interp = ref GrammarInterpMap.empty
 
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
+let (grammar_state : (int * GrammarCommand.t) list ref) = ref []
 
-type all_grammar_command =
-  | Notation of Notation.level * notation_grammar
-  | TacticGrammar of KerName.t * tactic_grammar
-  | MLTacticGrammar of ml_tactic_name * Tacexpr.raw_tactic_expr grammar_prod_item list list
+type 'a grammar_command = 'a GrammarCommand.tag
 
-(** ML Tactic grammar extensions *)
+let create_grammar_command name interp : _ grammar_command =
+  let obj = GrammarCommand.create name in
+  let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
+  obj
 
-let add_ml_tactic_entry name prods =
-  let entry = Tactic.simple_tactic in
-  let mkact i loc l : raw_tactic_expr =
-    let open Tacexpr in
-    let entry = { mltac_name = name; mltac_index = i } in
-    let map arg = TacGeneric arg in
-    TacML (loc, entry, List.map map l)
-  in
-  let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (None, [(None, None, List.rev rules)]);
-  1
-
-(* Declaration of the tactic grammar rule *)
-
-let head_is_ident tg = match tg.tacgram_prods with
-| GramTerminal _::_ -> true
-| _ -> false
-
-(** Tactic grammar extensions *)
-
-let add_tactic_entry kn tg =
-  let entry, pos = get_tactic_entry tg.tacgram_level in
-  let mkact loc l =
-    let filter = function
-    | GramTerminal _ -> None
-    | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t)
-    in
-    let types = List.map_filter filter tg.tacgram_prods in
-    let map arg t =
-      (** HACK to handle especially the tactic(...) entry *)
-      let wit = Genarg.rawwit Constrarg.wit_tactic in
-      if Genarg.argument_type_eq t (Genarg.unquote wit) then
-        Tacexp (Genarg.out_gen wit arg)
-      else
-        TacGeneric arg
-    in
-    let l = List.map2 map l types in
-    (TacAlias (loc,kn,l):raw_tactic_expr)
-  in
-  let () =
-    if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
-      error "Notation for simple tactic must start with an identifier."
-  in
-  let rules = make_rule mkact tg.tacgram_prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
-  1
-
-let (grammar_state : (int * all_grammar_command) list ref) = ref []
-
-let extend_grammar gram =
-  let nb = match gram with
-  | Notation (_,a) -> extend_constr_notation a
-  | TacticGrammar (kn, g) -> add_tactic_entry kn g
-  | MLTacticGrammar (name, pr) -> add_ml_tactic_entry name pr
-  in
-  grammar_state := (nb,gram) :: !grammar_state
+let extend_grammar tag g =
+  let nb = GrammarInterpMap.find tag !grammar_interp g in
+  grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
 
-let extend_constr_grammar pr ntn =
-  extend_grammar (Notation (pr, ntn))
+let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
 
-let extend_tactic_grammar kn ntn =
-  extend_grammar (TacticGrammar (kn, ntn))
+let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag =
+  create_grammar_command "Notation" extend_constr_notation
 
-let extend_ml_tactic_grammar name ntn =
-  extend_grammar (MLTacticGrammar (name, ntn))
+let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn)
 
 let recover_constr_grammar ntn prec =
-  let filter = function
-  | _, Notation (prec', ng) when
-      Notation.level_eq prec prec' &&
-      String.equal ntn ng.notgram_notation -> Some ng
-  | _ -> None
+  let filter (_, gram) : notation_grammar option = match gram with
+  | GrammarCommand.Dyn (tag, obj) ->
+    match GrammarCommand.eq tag constr_grammar with
+    | None -> None
+    | Some Refl ->
+      let (prec', ng) = obj in
+      if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
+      else None
   in
   match List.map_filter filter !grammar_state with
   | [x] -> x
@@ -334,7 +267,7 @@ let recover_constr_grammar ntn prec =
 (* Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
-type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
+type frozen_t = (int * GrammarCommand.t) list * Lexer.frozen_t
 
 let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
 
@@ -353,7 +286,7 @@ let unfreeze (grams, lex) =
   remove_levels n;
   grammar_state := common;
   Lexer.unfreeze lex;
-  List.iter extend_grammar (List.rev_map snd redo)
+  List.iter extend_dyn_grammar (List.rev_map snd redo)
 
 (** No need to provide an init function : the grammar state is
     statically available, and already empty initially, while
@@ -373,33 +306,3 @@ let with_grammar_rule_protection f x =
     let reraise = Errors.push reraise in
     let () = unfreeze fs in
     iraise reraise
-
-(**********************************************************************)
-(** Ltac quotations                                                   *)
-
-let ltac_quotations = ref String.Set.empty
-
-let create_ltac_quotation name cast (e, l) =
-  let () =
-    if String.Set.mem name !ltac_quotations then
-      failwith ("Ltac quotation " ^ name ^ " already registered")
-  in
-  let () = ltac_quotations := String.Set.add name !ltac_quotations in
-  let entry = match l with
-  | None -> Aentry (name_of_entry e)
-  | Some l -> Aentryl (name_of_entry e, l)
-  in
-(*   let level = Some "1" in *)
-  let level = None in
-  let assoc = None in
-  let rule =
-    Next (Next (Next (Next (Next (Stop,
-      Atoken (Lexer.terminal name)),
-      Atoken (Lexer.terminal ":")),
-      Atoken (Lexer.terminal "(")),
-      entry),
-      Atoken (Lexer.terminal ")"))
-  in
-  let action _ v _ _ _ loc = cast (loc, v) in
-  let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 23eaa64eec..6ec1066260 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -36,34 +36,27 @@ type notation_grammar = {
   notgram_typs : notation_var_internalization_type list;
 }
 
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
+(** {5 Extending the parser with Summary-synchronized commands} *)
+
+type 'a grammar_command
+(** Type of synchronized parsing extensions. The ['a] type should be
+    marshallable. *)
+
+val create_grammar_command : string -> ('a -> int) -> 'a grammar_command
+(** Create a new grammar-modifying command with the given name. The function
+    should modify the parser state and return the number of grammar extensions
+    performed. *)
+
+val extend_grammar : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
 
 (** {5 Adding notations} *)
 
 val extend_constr_grammar : Notation.level -> notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
 
-val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
-(** Add a tactic notation rule to the parsing system. This produces a TacAlias
-    tactic with the provided kernel name. *)
-
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit
-(** Add a ML tactic notation rule to the parsing system. This produces a
-    TacML tactic with the provided string as name. *)
-
 val recover_constr_grammar : notation -> Notation.level -> notation_grammar
 (** For a declared grammar, returns the rule + the ordered entry types
     of variables in the rule (for use in the interpretation) *)
 
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-
-(** {5 Adding tactic quotations} *)
-
-val create_ltac_quotation : string ->
-  ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit
-(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
-    Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
-    generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 207b43064c..75144addb2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -57,16 +57,6 @@ type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a G.entry -> ty
 let object_of_typed_entry (TypedEntry (_, e)) = Gramobj.weaken_entry e
 let weaken_entry x = Gramobj.weaken_entry x
 
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) symbol -> entry_name
-
 (** Grammar extensions *)
 
 (** NB: [extend_statment =
@@ -740,108 +730,8 @@ let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   unsafe_grammar_extend e reinit ext
 
-(**********************************************************************)
-(* Interpret entry names of the form "ne_constr_list" as entry keys   *)
-
-let coincide s pat off =
-  let len = String.length pat in
-  let break = ref true in
-  let i = ref 0 in
-  while !break && !i < len do
-    let c = Char.code s.[off + !i] in
-    let d = Char.code pat.[!i] in
-    break := Int.equal c d;
-    incr i
-  done;
-  !break
-
 let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
 
-let atactic n =
-  if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
-  else Aentryl (name_of_entry Tactic.tactic_expr, n)
-
-let try_get_entry u s =
-  (** Order the effects: get_entry can raise Not_found *)
-  let TypedEntry (typ, e) = get_entry u s in
-  EntryName (typ, Aentry (name_of_entry e))
-
-(** Quite ad-hoc *)
-let get_tacentry n m =
-  let check_lvl n =
-    Int.equal m n
-    && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
-    && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
-  in
-  if check_lvl n then EntryName (rawwit wit_tactic, Aself)
-  else if check_lvl (n + 1) then EntryName (rawwit wit_tactic, Anext)
-  else EntryName (rawwit wit_tactic, atactic n)
-
-let rec parse_user_entry s sep =
-  let l = String.length s in
-  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
-    Ulist1 entry
-  else if l > 12 && coincide s "ne_" 0 &&
-                   coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
-    Ulist1sep (entry, sep)
-  else if l > 5 && coincide s "_list" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
-    Ulist0 entry
-  else if l > 9 && coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
-    Ulist0sep (entry, sep)
-  else if l > 4 && coincide s "_opt" (l-4) then
-    let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
-    Uopt entry
-  else if l > 5 && coincide s "_mods" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
-    Umodifiers entry
-  else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
-    let n = Char.code s.[6] - 48 in
-    Uentryl ("tactic", n)
-  else
-    let s = match s with "hyp" -> "var" | _ -> s in
-    Uentry s
-
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
-let rec interp_entry_name up_level s sep =
-  let rec eval = function
-  | Ulist1 e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist1 g)
-  | Ulist1sep (e, sep) ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist1sep (g, sep))
-  | Ulist0 e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist0 g)
-  | Ulist0sep (e, sep) ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist0sep (g, sep))
-  | Uopt e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_opt t, Aopt g)
-  | Umodifiers e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Amodifiers g)
-  | Uentry s ->
-    begin
-      try try_get_entry uprim s with Not_found ->
-      try try_get_entry uconstr s with Not_found ->
-      try try_get_entry utactic s with Not_found ->
-      error ("Unknown entry "^s^".")
-    end
-  | Uentryl (s, n) ->
-    (** FIXME: do better someday *)
-    assert (String.equal s "tactic");
-    get_tacentry n up_level
-  in
-  eval (parse_user_entry s sep)
-
 let list_entry_names () =
   let add_entry key (TypedEntry (entry, _)) accu = (key, unquote entry) :: accu in
   let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 35973a4d72..afe8889096 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -268,13 +268,9 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** Binding general entry keys to symbols *)
 
-type entry_name = EntryName :
-  'a raw_abstract_argument_type * (raw_tactic_expr, 'a) Extend.symbol -> entry_name
+type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
 
-(** [interp_entry_name lev n sep] returns the entry corresponding to the name
-    [n] of the form "ne_constr_list" in a tactic entry of level [lev] with
-    separator [sep]. *)
-val interp_entry_name : int -> string -> string -> entry_name
+val get_entry : gram_universe -> string -> typed_entry
 
 (** Recover the list of all known tactic notation entries. *)
 val list_entry_names : unit -> (string * argument_type) list
diff --git a/test-suite/bugs/closed/1850.v b/test-suite/bugs/closed/1850.v
new file mode 100644
index 0000000000..26b48093b7
--- /dev/null
+++ b/test-suite/bugs/closed/1850.v
@@ -0,0 +1,4 @@
+Parameter P : Type -> Type -> Type.
+Notation      "e |= t --> v" := (P e t v)     (at level 100, t at level 54).
+Fail Check (nat |= nat --> nat).
+