5 files changed, 27 insertions, 15 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index b5ab3a87b..dab81c8ef 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -181,7 +181,7 @@ let declare_tactic loc s c cl =
 	  (Pp.app
 	     (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
 	     (Errors.print e)) ];
-      Egramml.extend_tactic_grammar $se$ $gl$;
+      Egramcoq.extend_ml_tactic_grammar $se$ $gl$;
       List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } >>
     ]
 
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index e2b78d725..1a25eabe5 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -252,6 +252,17 @@ type tactic_grammar = {
 type all_grammar_command =
   | Notation of Notation.level * notation_grammar
   | TacticGrammar of KerName.t * tactic_grammar
+  | MLTacticGrammar of string * grammar_prod_item list list
+
+(** ML Tactic grammar extensions *)
+
+let add_ml_tactic_entry name prods =
+  let entry = weaken_entry Tactic.simple_tactic in
+  let mkact loc l = Tacexpr.TacExtend (loc, name, List.map snd l) in
+  let rules = List.map (make_rule mkact) prods in
+  synchronize_level_positions ();
+  grammar_extend entry None (None ,[(None, None, List.rev rules)]);
+  1
 
 (* Declaration of the tactic grammar rule *)
 
@@ -259,6 +270,8 @@ 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 rules =
@@ -282,7 +295,9 @@ 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 in
+  | 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_constr_grammar pr ntn =
@@ -291,6 +306,9 @@ let extend_constr_grammar pr ntn =
 let extend_tactic_grammar kn ntn =
   extend_grammar (TacticGrammar (kn, ntn))
 
+let extend_ml_tactic_grammar name ntn =
+  extend_grammar (MLTacticGrammar (name, ntn))
+
 let recover_constr_grammar ntn prec =
   let filter = function
   | _, Notation (prec', ng) when
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index ee6ed4a9e..b51c19f7a 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -47,7 +47,12 @@ 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. *)
+(** Add a tactic notation rule to the parsing system. This produces a TacAlias
+    tactic with the provided kernel name. *)
+
+val extend_ml_tactic_grammar : string -> grammar_prod_item list list -> unit
+(** Add a ML tactic notation rule to the parsing system. This produces a
+    TacExtend 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
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index f26ff817b..51dda2664 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -42,14 +42,6 @@ let make_rule mkact pt =
   let act = make_generic_action mkact ntl in
   (symbs, act)
 
-(** Tactic grammar extensions *)
-
-let extend_tactic_grammar s gl =
-  let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
-  let rules = List.map (make_rule mkact) gl in
-  maybe_uncurry (Gram.extend Tactic.simple_tactic)
-    (None,[(None, None, List.rev rules)])
-
 (** Vernac grammar extensions *)
 
 let vernac_exts = ref []
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 87c0bcf45..9e2c29b98 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -8,7 +8,7 @@
 
 (** Mapping of grammar productions to camlp4 actions. *)
 
-(** This is the part specific to ML-level tactic and vernac extensions.
+(** This is the part specific to vernac extensions.
     For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
 
 type grammar_prod_item =
@@ -16,9 +16,6 @@ type grammar_prod_item =
   | GramNonTerminal of Loc.t * Genarg.argument_type *
       Pcoq.prod_entry_key * Names.Id.t option
 
-val extend_tactic_grammar :
-  string -> grammar_prod_item list list -> unit
-
 val extend_vernac_command_grammar :
   string -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
     grammar_prod_item list list -> unit