Simplifying and uniformizing the implementation of tactic notations.

This branch mainly provides two features:

1. The resolution of tactic notation scopes is not tied to a hardwired Pcoq
registration anymore. We expose instead an API to interpret names as a given
generic argument, effectively reversing the logical dependency between parsing
entries and generic arguments.

2. ML tactics do not declare their own notation system anymore. They rely instead
on plain tactic notations, except for a little hack due to the way we currently
interpret toplevel values.

12 files changed, 201 insertions, 206 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 2ef30f299b..19b6e1b5f6 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -45,26 +45,30 @@ let make_fun_clauses loc s l =
   let map c = Compat.make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
+let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >>
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+  let arg = get_argt <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  let arg = get_argt <:expr< Constrarg.wit_tactic >> in
+  <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
+
 let make_prod_item = function
-  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+  | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
   | ExtNonTerminal (g, id) ->
-    let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
-      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key base g$ >>
+    <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >>
 
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
 
-let make_one_printing_rule (pt,_,e) =
-  let level = mlexpr_of_int 0 in (* only level 0 supported here *)
-  let loc = MLast.loc_of_expr e in
-  let prods = mlexpr_of_list make_prod_item pt in
-  <:expr< { Pptactic.pptac_level = $level$;
-            pptac_prods = $prods$ } >>
-
-let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
-
 (** Special treatment of constr entries *)
 let is_constr_gram = function
 | ExtTerminal _ -> false
@@ -118,15 +122,13 @@ let declare_tactic loc s c cl = match cl with
       TacML tactic. *)
   let entry = mlexpr_of_string s in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
   let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
       try do {
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
-        Mltop.declare_cache_obj $obj$ $plugin_name$;
-        Pptactic.declare_ml_tactic_pprule $se$ (Array.of_list $pp$); }
+        Mltop.declare_cache_obj $obj$ $plugin_name$; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
           (Pp.app
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index aedaead71a..0d4bec69d5 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -102,6 +102,14 @@ let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
   mlexpr_of_list (fun x -> x) cl
 
+let make_prod_item = function
+  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+  | ExtNonTerminal (g, id) ->
+    let nt = type_of_user_symbol g in
+    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
+      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
+      $mlexpr_of_prod_entry_key base g$ >>
+
 let mlexpr_of_clause cl =
   let mkexpr { r_head = a; r_patt = b; } = match a with
   | None -> mlexpr_of_list make_prod_item b
diff --git a/intf/extend.mli b/intf/extend.mli
index 10713745e4..381d47dd18 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -53,14 +53,14 @@ type simple_constr_prod_entry_key =
 
 (** {5 AST for user-provided entries} *)
 
-type user_symbol =
-| Ulist1 : user_symbol -> user_symbol
-| Ulist1sep : user_symbol * string -> user_symbol
-| Ulist0 : user_symbol -> user_symbol
-| Ulist0sep : user_symbol * string -> user_symbol
-| Uopt : user_symbol -> user_symbol
-| Uentry : string -> user_symbol
-| Uentryl : string * int -> user_symbol
+type 'a user_symbol =
+| Ulist1 of 'a user_symbol
+| Ulist1sep of 'a user_symbol * string
+| Ulist0 of 'a user_symbol
+| Ulist0sep of 'a user_symbol * string
+| Uopt of 'a user_symbol
+| Uentry of 'a
+| Uentryl of 'a * int
 
 (** {5 Type-safe grammar extension} *)
 
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index fbae17bafc..0bddcc9fdd 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -40,6 +40,16 @@ let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
   Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
 
+(** Backward-compatible tactic notation entry names *)
+
+let () =
+  let register name entry = Tacentries.register_tactic_notation_entry name entry in
+  register "hyp" wit_var;
+  register "simple_intropattern" wit_intro_pattern;
+  register "integer" wit_integer;
+  register "reference" wit_ref;
+  ()
+
 (* Rewriting orientation *)
 
 let _ = Metasyntax.add_token_obj "<-"
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index fe750f429f..df499a2c9c 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -405,7 +405,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation
   [
     let l = Locality.LocalityFixme.consume () in
     let n = Option.default 0 n in
-    Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e)
+    Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e
   ]
 END
 
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 46e48c6953..f94f84a73b 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -23,6 +23,9 @@ type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
 | TacNonTerm of Loc.t * 'a * Names.Id.t
 
+type raw_argument = string * string option
+type argument = Genarg.ArgT.any Extend.user_symbol
+
 (**********************************************************************)
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
@@ -46,12 +49,6 @@ let atactic 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
@@ -91,13 +88,12 @@ let rec parse_user_entry s sep =
     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 interp_entry_name interp symb =
   let open Extend in
   let rec eval = function
   | Ulist1 e ->
@@ -115,19 +111,10 @@ let interp_entry_name up_level s sep =
   | Uopt e ->
     let EntryName (t, g) = eval e in
     EntryName (arg_opt t, Aopt 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
+  | Uentry s -> interp s None
+  | Uentryl (s, n) -> interp s (Some n)
   in
-  eval (parse_user_entry s sep)
+  eval symb
 
 (**********************************************************************)
 (** Grammar declaration for Tactic Notation (Coq level)               *)
@@ -150,21 +137,6 @@ type tactic_grammar = {
   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
@@ -173,7 +145,7 @@ let head_is_ident tg = match tg.tacgram_prods with
 
 (** Tactic grammar extensions *)
 
-let add_tactic_entry (kn, tg) =
+let add_tactic_entry (kn, ml, tg) =
   let open Tacexpr in
   let entry, pos = get_tactic_entry tg.tacgram_level in
   let mkact loc l =
@@ -185,7 +157,7 @@ let add_tactic_entry (kn, tg) =
     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
+      if Genarg.argument_type_eq t (Genarg.unquote wit) && not ml then
         Tacexp (Genarg.out_gen wit arg)
       else
         TacGeneric arg
@@ -205,24 +177,42 @@ let add_tactic_entry (kn, tg) =
 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)
+let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn)
 
 (**********************************************************************)
 (* Tactic Notation                                                    *)
 
+let entry_names = ref String.Map.empty
+
+let register_tactic_notation_entry name entry =
+  let entry = match entry with
+  | ExtraArg arg -> ArgT.Any arg
+  | _ -> assert false
+  in
+  entry_names := String.Map.add name entry !entry_names
+
 let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, (nt, sep), _) ->
-      let EntryName (etyp, e) = interp_entry_name lev nt sep in
-      GramNonTerminal (loc, etyp, e)
-
-let make_terminal_status = function
-  | GramTerminal s -> Some s
-  | GramNonTerminal _ -> None
+    let symbol = parse_user_entry nt sep in
+    let interp s = function
+    | None ->
+      let ArgT.Any arg =
+        if String.Map.mem s !entry_names then
+          String.Map.find s !entry_names
+        else match ArgT.name s with
+        | None -> error ("Unknown entry "^s^".")
+        | Some arg -> arg
+      in
+      let wit = ExtraArg arg in
+      EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit)))
+    | Some n ->
+      (** FIXME: do better someday *)
+      assert (String.equal s "tactic");
+      get_tacentry n lev
+    in
+    let EntryName (etyp, e) = interp_entry_name interp symbol in
+    GramNonTerminal (loc, etyp, e)
 
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -243,8 +233,13 @@ type tactic_grammar_obj = {
   tacobj_key : KerName.t;
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
-  tacobj_tacpp : Pptactic.pp_tactic;
   tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+  tacobj_forml : bool;
+}
+
+let pprule pa = {
+  Pptactic.pptac_level = pa.tacgram_level;
+  pptac_prods = pa.tacgram_prods;
 }
 
 let check_key key =
@@ -256,22 +251,22 @@ let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
   let () = check_key key in
   Tacenv.register_alias key tobj.tacobj_body;
-  extend_tactic_grammar key tobj.tacobj_tacgram;
-  Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
+  extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram;
+  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram)
 
 let open_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
   if Int.equal i 1 && not tobj.tacobj_local then
-    extend_tactic_grammar key tobj.tacobj_tacgram
+    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
 
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
   let () = check_key key in
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
-  Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
+  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram);
   if Int.equal i 1 && not tobj.tacobj_local then
-    extend_tactic_grammar key tobj.tacobj_tacgram
+    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
   let (ids, body) = tobj.tacobj_body in
@@ -294,14 +289,7 @@ let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, _, id) -> Some id
 
-let add_tactic_notation (local,n,prods,e) =
-  let ids = List.map_filter cons_production_parameter prods in
-  let prods = List.map (interp_prod_item n) prods in
-  let pprule = {
-    Pptactic.pptac_level = n;
-    pptac_prods = prods;
-  } in
-  let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
+let add_glob_tactic_notation local n prods forml ids tac =
   let parule = {
     tacgram_level = n;
     tacgram_prods = prods;
@@ -310,21 +298,20 @@ let add_tactic_notation (local,n,prods,e) =
     tacobj_key = make_fresh_key ();
     tacobj_local = local;
     tacobj_tacgram = parule;
-    tacobj_tacpp = pprule;
     tacobj_body = (ids, tac);
+    tacobj_forml = forml;
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)
 
+let add_tactic_notation local n prods e =
+  let ids = List.map_filter cons_production_parameter prods in
+  let prods = List.map (interp_prod_item n) prods in
+  let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
+  add_glob_tactic_notation local n prods false ids tac
+
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
 
-type ml_tactic_grammar_obj = {
-  mltacobj_name : Tacexpr.ml_tactic_name;
-  (** ML-side unique name *)
-  mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list;
-  (** Grammar rules generating the ML tactic. *)
-}
-
 exception NonEmptyArgument
 
 (** ML tactic notations whose use can be restricted to an identifier are added
@@ -359,27 +346,33 @@ let extend_atomic_tactic name entries =
   in
   List.iteri add_atomic entries
 
-let cache_ml_tactic_notation (_, obj) =
-  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
-
-let open_ml_tactic_notation i obj =
-  if Int.equal i 1 then cache_ml_tactic_notation obj
-
-let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
-  declare_object { (default_object "MLTacticGrammar") with
-    open_function = open_ml_tactic_notation;
-    cache_function = cache_ml_tactic_notation;
-    classify_function = (fun o -> Substitute o);
-    subst_function = (fun (_, o) -> o);
-  }
-
 let add_ml_tactic_notation name prods =
-  let obj = {
-    mltacobj_name = name;
-    mltacobj_prod = prods;
-  } in
-  Lib.add_anonymous_leaf (inMLTacticGrammar obj);
-  extend_atomic_tactic name prods
+  let interp_prods = function
+  | TacTerm s -> None, GramTerminal s
+  | TacNonTerm (loc, symb, id) ->
+    let interp (ArgT.Any tag) lev = match lev with
+    | None ->
+      let wit = ExtraArg tag in
+      EntryName (Rawwit wit, Extend.Aentry (Pcoq.name_of_entry (Pcoq.genarg_grammar wit)))
+    | Some lev ->
+      assert (coincide (ArgT.repr tag) "tactic" 0);
+      EntryName (Rawwit Constrarg.wit_tactic, atactic lev)
+    in
+    let EntryName (etyp, e) = interp_entry_name interp symb in
+    Some id, GramNonTerminal (loc, etyp, e)
+  in
+  let prods = List.map (fun p -> List.map interp_prods p) prods in
+  let iter i prods =
+    let open Tacexpr in
+    let (ids, prods) = List.split prods in
+    let ids = List.map_filter (fun x -> x) ids in
+    let entry = { mltac_name = name; mltac_index = i } in
+    let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
+    let tac = TacML (Loc.ghost, entry, List.map map ids) in
+    add_glob_tactic_notation false 0 prods true ids tac
+  in
+  List.iteri iter prods;
+  extend_atomic_tactic name (List.map (fun p -> List.map snd p) prods)
 
 (**********************************************************************)
 (** Ltac quotations                                                   *)
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 0f4bb2530e..7586bff92f 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -6,25 +6,51 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Ltac toplevel command entries. *)
+
 open Vernacexpr
 open Tacexpr
 
+(** {5 Tactic Definitions} *)
+
+val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit
+(** Adds new Ltac definitions to the environment. *)
+
+(** {5 Tactic Notations} *)
+
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
 | TacNonTerm of Loc.t * 'a * Names.Id.t
 
-(** Adding a tactic notation in the environment *)
+type raw_argument = string * string option
+(** An argument type as provided in Tactic notations, i.e. a string like
+    "ne_foo_list_opt" together with a separator that only makes sense in the
+    "_sep" cases. *)
+
+type argument = Genarg.ArgT.any Extend.user_symbol
+(** A fully resolved argument type given as an AST with generic arguments on the
+    leaves. *)
 
 val add_tactic_notation :
-  locality_flag * int * (string * string option) grammar_tactic_prod_item_expr list * raw_tactic_expr ->
-    unit
+  locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
+  raw_tactic_expr -> unit
+(** [add_tactic_notation local level prods expr] adds a tactic notation in the
+    environment at level [level] with locality [local] made of the grammar
+    productions [prods] and returning the body [expr] *)
+
+val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -> unit
+(** Register an argument under a given entry name for tactic notations. When
+    translating [raw_argument] into [argument], atomic names will be first
+    looked up according to names registered through this function and fallback
+    to finding an argument by name (as in {!Genarg}) if there is none
+    matching. *)
 
 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
+  argument grammar_tactic_prod_item_expr list list -> unit
+(** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
+    ML-side macro. *)
 
-(** {5 Adding tactic quotations} *)
+(** {5 Tactic Quotations} *)
 
 val create_ltac_quotation : string ->
   ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 802c24eef4..e60b470fdf 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -12,8 +12,6 @@ open Errors
 open Util
 open Extend
 open Genarg
-open Stdarg
-open Constrarg
 open Tok (* necessary for camlp4 *)
 
 (** The parser of Coq *)
@@ -53,8 +51,6 @@ end
 (** Grammar entries with associated types *)
 
 type grammar_object = Gramobj.grammar_object
-type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a G.entry -> typed_entry
-let object_of_typed_entry (TypedEntry (_, e)) = Gramobj.weaken_entry e
 let weaken_entry x = Gramobj.weaken_entry x
 
 (** Grammar extensions *)
@@ -177,12 +173,11 @@ let parse_string f x =
 
 type gram_universe = string
 
-let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t =
+let utables : (string, unit) Hashtbl.t =
   Hashtbl.create 97
 
 let create_universe u =
-  let table = Hashtbl.create 97 in
-  let () = Hashtbl.add utables u table in
+  let () = Hashtbl.add utables u () in
   u
 
 let uprim   = create_universe "prim"
@@ -194,14 +189,6 @@ let get_univ u =
   if Hashtbl.mem utables u then u
   else raise Not_found
 
-let get_utable u =
-  try Hashtbl.find utables u
-  with Not_found -> assert false
-
-let get_entry u s =
-  let utab = get_utable u in
-  Hashtbl.find utab s
-
 (** A table associating grammar to entries *)
 let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
 
@@ -212,15 +199,14 @@ let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) =
   assert (not (String.Map.mem (Entry.repr e) !gtable));
   gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable
 
-let new_entry etyp u s =
-  let utab = get_utable u in
+let new_entry u s =
   let ename = u ^ ":" ^ s in
   let entry = Entry.create ename in
   let e = Gram.entry_create ename in
   let () = set_grammar entry e in
-  Hashtbl.add utab s (TypedEntry (etyp, e)); e
+  e
 
-let make_gen_entry u rawwit s = new_entry rawwit u s
+let make_gen_entry u s = new_entry u s
 
 module GrammarObj =
 struct
@@ -235,36 +221,32 @@ let register_grammar = Grammar.register0
 let genarg_grammar = Grammar.obj
 
 let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
-  let utab = get_utable u in
-  if Hashtbl.mem utab s then
-    failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists")
-  else
-    let e = new_entry etyp u s in
-    let Rawwit t = etyp in
-    let () = Grammar.register0 t e in
-    e
+  let e = new_entry u s in
+  let Rawwit t = etyp in
+  let () = Grammar.register0 t e in
+  e
 
 (* Initial grammar entries *)
 
 module Prim =
   struct
-    let gec_gen x = make_gen_entry uprim x
+    let gec_gen n = make_gen_entry uprim n
 
     (* Entries that can be referred via the string -> Gram.entry table *)
     (* Typically for tactic or vernac extensions *)
-    let preident = gec_gen (rawwit wit_pre_ident) "preident"
-    let ident = gec_gen (rawwit wit_ident) "ident"
-    let natural = gec_gen (rawwit wit_int) "natural"
-    let index = gec_gen (rawwit wit_int) "index"
-    let integer = gec_gen (rawwit wit_int) "integer"
+    let preident = gec_gen "preident"
+    let ident = gec_gen "ident"
+    let natural = gec_gen "natural"
+    let index = gec_gen "index"
+    let integer = gec_gen "integer"
     let bigint = Gram.entry_create "Prim.bigint"
-    let string = gec_gen (rawwit wit_string) "string"
-    let reference = make_gen_entry uprim (rawwit wit_ref) "reference"
+    let string = gec_gen "string"
+    let reference = make_gen_entry uprim "reference"
     let by_notation = Gram.entry_create "by_notation"
     let smart_global = Gram.entry_create "smart_global"
 
     (* parsed like ident but interpreted as a term *)
-    let var = gec_gen (rawwit wit_var) "var"
+    let var = gec_gen "var"
 
     let name = Gram.entry_create "Prim.name"
     let identref = Gram.entry_create "Prim.identref"
@@ -286,7 +268,7 @@ module Prim =
 
 module Constr =
   struct
-    let gec_constr = make_gen_entry uconstr (rawwit wit_constr)
+    let gec_constr = make_gen_entry uconstr
 
     (* Entries that can be referred via the string -> Gram.entry table *)
     let constr = gec_constr "constr"
@@ -294,9 +276,9 @@ module Constr =
     let constr_eoi = eoi_entry constr
     let lconstr = gec_constr "lconstr"
     let binder_constr = gec_constr "binder_constr"
-    let ident = make_gen_entry uconstr (rawwit wit_ident) "ident"
-    let global = make_gen_entry uconstr (rawwit wit_ref) "global"
-    let sort = make_gen_entry uconstr (rawwit wit_sort) "sort"
+    let ident = make_gen_entry uconstr "ident"
+    let global = make_gen_entry uconstr "global"
+    let sort = make_gen_entry uconstr "sort"
     let pattern = Gram.entry_create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
@@ -324,32 +306,32 @@ module Tactic =
     (* Entries that can be referred via the string -> Gram.entry table *)
     (* Typically for tactic user extensions *)
     let open_constr =
-      make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
+      make_gen_entry utactic "open_constr"
     let constr_with_bindings =
-      make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
+      make_gen_entry utactic "constr_with_bindings"
     let bindings =
-      make_gen_entry utactic (rawwit wit_bindings) "bindings"
+      make_gen_entry utactic "bindings"
     let hypident = Gram.entry_create "hypident"
-    let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
-    let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_eval"
+    let constr_may_eval = make_gen_entry utactic "constr_may_eval"
+    let constr_eval = make_gen_entry utactic "constr_eval"
     let uconstr =
-      make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
+      make_gen_entry utactic "uconstr"
     let quantified_hypothesis =
-      make_gen_entry utactic (rawwit wit_quant_hyp) "quantified_hypothesis"
-    let int_or_var = make_gen_entry utactic (rawwit wit_int_or_var) "int_or_var"
-    let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr"
+      make_gen_entry utactic "quantified_hypothesis"
+    let int_or_var = make_gen_entry utactic "int_or_var"
+    let red_expr = make_gen_entry utactic "red_expr"
     let simple_intropattern =
-      make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern"
+      make_gen_entry utactic "simple_intropattern"
     let clause_dft_concl = 
-      make_gen_entry utactic (rawwit wit_clause_dft_concl) "clause"
+      make_gen_entry utactic "clause"
 
 
     (* Main entries for ltac *)
     let tactic_arg = Gram.entry_create "tactic:tactic_arg"
-    let tactic_expr = make_gen_entry utactic (rawwit wit_tactic)  "tactic_expr"
-    let binder_tactic = make_gen_entry utactic (rawwit wit_tactic) "binder_tactic"
+    let tactic_expr = make_gen_entry utactic "tactic_expr"
+    let binder_tactic = make_gen_entry utactic "binder_tactic"
 
-    let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
+    let tactic = make_gen_entry utactic "tactic"
 
     (* Main entry for quotations *)
     let tactic_eoi = eoi_entry tactic
@@ -593,9 +575,7 @@ let compute_entry adjust forpat = function
   | ETReference -> weaken_entry Constr.global, None, false
   | ETPattern -> weaken_entry Constr.pattern, None, false
   | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
-  | ETOther (u,n) ->
-      let e = get_entry u n in
-      object_of_typed_entry e, None, true
+  | ETOther (u,n) -> assert false
 
 (* This computes the name of the level where to add a new rule *)
 let interp_constr_entry_key forpat level =
@@ -725,11 +705,7 @@ let grammar_extend e reinit ext =
 
 let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
 
-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
-  let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in
-  Hashtbl.fold add_entry (get_utable utactic) ans
+let list_entry_names () = []
 
 let epsilon_value f e =
   let r = Rule (Next (Stop, e), fun x _ -> f x) in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index afe8889096..d320520015 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -268,10 +268,6 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** Binding general entry keys to symbols *)
 
-type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
-
-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/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8baa668c7b..5e6a3eac73 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1126,7 +1126,7 @@ let type_uconstr ?(flags = constr_flags)
     ltac_constrs = closure.typed;
     ltac_uconstrs = closure.untyped;
     ltac_idents = closure.idents;
-    ltac_genargs = ist.Geninterp.lfun;
+    ltac_genargs = Id.Map.empty;
   } in
   let sigma = Sigma.to_evar_map sigma in
   let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 19536d9f83..631cb4c577 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -33,16 +33,9 @@ type pp_tactic = {
   pptac_prods : grammar_terminals;
 }
 
-(* ML Extensions *)
-let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t =
-  Hashtbl.create 17
-
 (* Tactic notations *)
 let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
 
-let declare_ml_tactic_pprule key pt =
-  Hashtbl.add prtac_tab key pt
-
 let declare_notation_tactic_pprule kn pt =
   prnotation_tab := KNmap.add kn pt !prnotation_tab
 
@@ -371,14 +364,6 @@ module Make
     pr_sequence (fun x -> x) l
 
   let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
-    try
-      let pp_rules = Hashtbl.find prtac_tab s in
-      let pp = pp_rules.(i) in
-      let args = List.map_filter filter_arg pp.pptac_prods in
-      let () = if not (List.for_all2eq check args l) then raise Not_found in
-      let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
-      if pp.pptac_level > lev then surround p else p
-    with Not_found ->
       let name =
         str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
         str "@" ++ int i
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 31a5a5d4a8..1608cae751 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -48,7 +48,6 @@ type pp_tactic = {
   pptac_prods : grammar_terminals;
 }
 
-val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 (** The default pretty-printers produce {!Pp.std_ppcmds} that are