From f3515efc26a693f4c525ad91c37c982f4c96e6ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 20 Apr 2016 23:24:02 +0200
Subject: Factorizing the declaration of ML notation printing in Tacentries.

---
 ltac/tacentries.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 46e48c6953..a3e15866ee 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -360,7 +360,13 @@ let extend_atomic_tactic name entries =
   List.iteri add_atomic entries
 
 let cache_ml_tactic_notation (_, obj) =
-  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
+  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod;
+  let pp_rule prods = {
+    Pptactic.pptac_level = 0 (* only level 0 supported here *);
+    pptac_prods = prods;
+  } in
+  let pp_rules = Array.map_of_list pp_rule obj.mltacobj_prod in
+  Pptactic.declare_ml_tactic_pprule obj.mltacobj_name pp_rules
 
 let open_ml_tactic_notation i obj =
   if Int.equal i 1 then cache_ml_tactic_notation obj
-- 
cgit v1.2.3


From b090942f20ac8854bf227698d31ca1efec492c47 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 Apr 2016 18:26:28 +0200
Subject: Higher-level API for tactic notations.

---
 ltac/g_ltac.ml4     |  2 +-
 ltac/tacentries.ml  | 52 ++++++++++++++++++++++++++++++++++++----------------
 ltac/tacentries.mli | 11 ++++++-----
 3 files changed, 43 insertions(+), 22 deletions(-)

(limited to 'ltac')

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 a3e15866ee..dfcfdece62 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -97,7 +97,7 @@ let rec parse_user_entry s sep =
 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 +115,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)               *)
@@ -217,8 +208,22 @@ let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
 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 symbol = parse_user_entry nt sep in
+    let interp s = function
+    | None ->
+      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
+    | 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_terminal_status = function
   | GramTerminal s -> Some s
@@ -294,7 +299,7 @@ let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, _, id) -> Some id
 
-let add_tactic_notation (local,n,prods,e) =
+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 = {
@@ -380,6 +385,21 @@ let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
   }
 
 let add_ml_tactic_notation name prods =
+  let interp_prods = function
+  | TacTerm s -> GramTerminal s
+  | TacNonTerm (loc, symb, _) ->
+    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
+    GramNonTerminal (loc, etyp, e)
+  in
+  let prods = List.map (fun p -> List.map interp_prods p) prods in
   let obj = {
     mltacobj_name = name;
     mltacobj_prod = prods;
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 0f4bb2530e..cd9f430cb7 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -13,14 +13,15 @@ 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 *)
-
 val add_tactic_notation :
-  locality_flag * int * (string * string option) grammar_tactic_prod_item_expr list * raw_tactic_expr ->
-    unit
+  locality_flag -> int -> (string * string option) 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 add_ml_tactic_notation : ml_tactic_name ->
-  Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
+  Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list list -> unit
 
 val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit
 
-- 
cgit v1.2.3


From ea984528e269fa34afa3dd1757a00ff5a8405157 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 24 Apr 2016 16:57:26 +0200
Subject: Disentangle tactic notation resolution from Pcoq.

Instead of relying on entry names as given by a hardwired registering
scheme in Pcoq, we recover them first through a user-defined map, and
fallback on generic argument names.
---
 ltac/extraargs.ml4  | 10 ++++++++++
 ltac/tacentries.ml  | 25 ++++++++++++++++++-------
 ltac/tacentries.mli |  3 +++
 3 files changed, 31 insertions(+), 7 deletions(-)

(limited to 'ltac')

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/tacentries.ml b/ltac/tacentries.ml
index dfcfdece62..2adeb3a655 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -91,7 +91,6 @@ 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)
@@ -205,18 +204,30 @@ let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, 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 symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
-      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
+      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");
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index cd9f430cb7..cdeb27ce69 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -20,6 +20,9 @@ val add_tactic_notation :
     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. *)
+
 val add_ml_tactic_notation : ml_tactic_name ->
   Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list list -> unit
 
-- 
cgit v1.2.3


From b1f95532137644d55b9018da80f9ffe63b289023 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 24 Apr 2016 17:35:02 +0200
Subject: Remove dead registering code in Pcoq.

---
 ltac/tacentries.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'ltac')

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 2adeb3a655..fc3dfc78dc 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -46,12 +46,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
-- 
cgit v1.2.3


From 3f5aa726ea075765ae7ec03d7f34f795cc6a1bc9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Apr 2016 08:32:04 +0200
Subject: Documenting API.

---
 ltac/tacentries.ml  |  3 +++
 ltac/tacentries.mli | 34 ++++++++++++++++++++++++++++------
 2 files changed, 31 insertions(+), 6 deletions(-)

(limited to 'ltac')

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index fc3dfc78dc..91eaa85228 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   *)
 
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index cdeb27ce69..7586bff92f 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -6,29 +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
 
+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 ->
+  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. *)
+(** 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 ->
-  Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr 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
-- 
cgit v1.2.3


From 27d4a57975ab5919d81f9951b430a35d1067e846 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Apr 2016 10:00:10 +0200
Subject: Factorizing code in tactic notations.

---
 ltac/tacentries.ml | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

(limited to 'ltac')

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 91eaa85228..c4569b98f7 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -233,10 +233,6 @@ let interp_prod_item lev = function
     let EntryName (etyp, e) = interp_entry_name interp symbol in
     GramNonTerminal (loc, etyp, e)
 
-let make_terminal_status = function
-  | GramTerminal s -> Some s
-  | GramNonTerminal _ -> None
-
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
   fun () ->
@@ -256,10 +252,14 @@ 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;
 }
 
+let pprule pa = {
+  Pptactic.pptac_level = pa.tacgram_level;
+  pptac_prods = pa.tacgram_prods;
+}
+
 let check_key key =
   if Tacenv.check_alias key then
     error "Conflicting tactic notations keys. This can happen when including \
@@ -270,7 +270,7 @@ let cache_tactic_notation (_, tobj) =
   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
+  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram)
 
 let open_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
@@ -282,7 +282,7 @@ let load_tactic_notation i (_, tobj) =
   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
 
@@ -310,10 +310,6 @@ let cons_production_parameter = function
 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 parule = {
     tacgram_level = n;
@@ -323,7 +319,6 @@ 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);
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)
-- 
cgit v1.2.3


From a7917a32b24b652d2978a7aea171aa01da37eece Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Apr 2016 10:55:38 +0200
Subject: Merging the ML tactic notation and plain Tactic Notation mechanisms.

---
 ltac/tacentries.ml | 94 +++++++++++++++++-------------------------------------
 1 file changed, 29 insertions(+), 65 deletions(-)

(limited to 'ltac')

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index c4569b98f7..f94f84a73b 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -137,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
@@ -160,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 =
@@ -172,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
@@ -192,11 +177,7 @@ 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                                                    *)
@@ -253,6 +234,7 @@ type tactic_grammar_obj = {
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
   tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+  tacobj_forml : bool;
 }
 
 let pprule pa = {
@@ -269,13 +251,13 @@ 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;
+  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
@@ -284,7 +266,7 @@ let load_tactic_notation i (_, tobj) =
   Tacenv.register_alias key tobj.tacobj_body;
   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
@@ -307,10 +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 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;
@@ -320,19 +299,19 @@ let add_tactic_notation local n prods e =
     tacobj_local = local;
     tacobj_tacgram = parule;
     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
@@ -367,30 +346,10 @@ 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 pp_rule prods = {
-    Pptactic.pptac_level = 0 (* only level 0 supported here *);
-    pptac_prods = prods;
-  } in
-  let pp_rules = Array.map_of_list pp_rule obj.mltacobj_prod in
-  Pptactic.declare_ml_tactic_pprule obj.mltacobj_name pp_rules
-
-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 interp_prods = function
-  | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, symb, _) ->
+  | TacTerm s -> None, GramTerminal s
+  | TacNonTerm (loc, symb, id) ->
     let interp (ArgT.Any tag) lev = match lev with
     | None ->
       let wit = ExtraArg tag in
@@ -400,15 +359,20 @@ let add_ml_tactic_notation name prods =
       EntryName (Rawwit Constrarg.wit_tactic, atactic lev)
     in
     let EntryName (etyp, e) = interp_entry_name interp symb in
-    GramNonTerminal (loc, etyp, e)
+    Some id, GramNonTerminal (loc, etyp, e)
   in
   let prods = List.map (fun p -> List.map interp_prods p) prods in
-  let obj = {
-    mltacobj_name = name;
-    mltacobj_prod = prods;
-  } in
-  Lib.add_anonymous_leaf (inMLTacticGrammar obj);
-  extend_atomic_tactic name prods
+  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                                                   *)
-- 
cgit v1.2.3