Moving the TacExtend node from atomic to plain tactics.

Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.

17 files changed, 117 insertions, 126 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 9631ed95e7..312f0e9497 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -197,10 +197,10 @@ let declare_tactic loc s c cl = match cl with
       let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
       <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
   in
-  (** Arguments are not passed directly to the ML tactic in the TacExtend node,
+  (** Arguments are not passed directly to the ML tactic in the TacML node,
       the ML tactic retrieves its arguments in the [ist] environment instead.
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
-  let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacAtom ($dloc$, Tacexpr.TacExtend($dloc$, $se$, []))) >> in
+  let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in
   let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in
   declare_str_items loc
     [ <:str_item< do {
@@ -216,7 +216,7 @@ let declare_tactic loc s c cl = match cl with
     ]
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
-      TacExtend tactic. *)
+      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 se cl in
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 8e5b51b873..b9c41ae03e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -162,9 +162,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option
   | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
 
-  (* For ML extensions *)
-  | TacExtend of Loc.t * ml_tactic_name * 'lev generic_argument list
-
   (* For syntax extensions *)
   | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list
 
@@ -247,6 +244,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
       ('p,('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr) match_rule list
   | TacFun of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast
   | TacArg of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_arg located
+  (* For ML extensions *)
+  | TacML of Loc.t * ml_tactic_name * 'l generic_argument list
 
 and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
     Id.t option list * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index e8072aa1a4..c56a5a7004 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -258,7 +258,7 @@ type all_grammar_command =
 
 let add_ml_tactic_entry name prods =
   let entry = weaken_entry Tactic.simple_tactic in
-  let mkact loc l : raw_atomic_tactic_expr = Tacexpr.TacExtend (loc, name, List.map snd l) in
+  let mkact loc l : raw_tactic_expr = Tacexpr.TacML (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)]);
@@ -274,18 +274,12 @@ let head_is_ident tg = match tg.tacgram_prods with
 
 let add_tactic_entry kn tg =
   let entry, pos = get_tactic_entry tg.tacgram_level in
-  let rules =
-    if Int.equal tg.tacgram_level 0 then begin
-      if not (head_is_ident tg) then
-        error "Notation for simple tactic must start with an identifier.";
-      let mkact loc l =
-        (TacAlias (loc,kn,l):raw_atomic_tactic_expr) in
-      make_rule mkact tg.tacgram_prods
-    end
-    else
-      let mkact loc l =
-        (TacAtom(loc,TacAlias(loc,kn,l)):raw_tactic_expr) in
-      make_rule mkact tg.tacgram_prods in
+  let mkact loc l = (TacAtom(loc, 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 (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
   1
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 2a5e89eb93..4cb55ee8e2 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -52,7 +52,7 @@ val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
 
 val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> 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. *)
+    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
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index ea38358660..ce3105548d 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -103,7 +103,7 @@ GEXTEND Gram
 	  l = LIST0 message_token -> TacFail (n,l)
       | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg ->
 	  TacArg (!@loc,TacExternal (!@loc,com,req,la))
-      | st = simple_tactic -> TacAtom (!@loc,st)
+      | st = simple_tactic -> st
       | IDENT "constr"; ":"; id = METAIDENT ->
           TacArg(!@loc,MetaIdArg (!@loc,false,id))
       | IDENT "constr"; ":"; c = Constr.constr ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a29c782c5b..2f9ab38d25 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -528,156 +528,156 @@ GEXTEND Gram
   simple_tactic:
     [ [
       (* Basic tactics *)
-        IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
+        IDENT "intros"; pl = intropatterns -> TacAtom (!@loc, TacIntroPattern pl)
       | IDENT "intro"; id = ident; hto = move_location ->
-	  TacIntroMove (Some id, hto)
-      | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto)
-      | IDENT "intro"; id = ident -> TacIntroMove (Some id, MoveLast)
-      | IDENT "intro" -> TacIntroMove (None, MoveLast)
+	  TacAtom (!@loc, TacIntroMove (Some id, hto))
+      | IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto))
+      | IDENT "intro"; id = ident -> TacAtom (!@loc, TacIntroMove (Some id, MoveLast))
+      | IDENT "intro" -> TacAtom (!@loc, TacIntroMove (None, MoveLast))
 
-      | IDENT "exact"; c = constr -> TacExact c
+      | IDENT "exact"; c = constr -> TacAtom (!@loc, TacExact c)
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
+          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
       | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp)
+          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,true,cl,inhyp))
       | IDENT "simple"; IDENT "apply";
           cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> TacApply (false,false,cl,inhyp)
+          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,false,cl,inhyp))
       | IDENT "simple"; IDENT "eapply";
           cl = LIST1 constr_with_bindings_arg SEP",";
-          inhyp = in_hyp_as -> TacApply (false,true,cl,inhyp)
+          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,true,cl,inhyp))
       | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
-          TacElim (false,cl,el)
+          TacAtom (!@loc, TacElim (false,cl,el))
       | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
-          TacElim (true,cl,el)
-      | IDENT "case"; icl = induction_clause_list -> mkTacCase false icl
-      | IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl
-      | "fix"; n = natural -> TacFix (None,n)
-      | "fix"; id = ident; n = natural -> TacFix (Some id,n)
+          TacAtom (!@loc, TacElim (true,cl,el))
+      | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl)
+      | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
+      | "fix"; n = natural -> TacAtom (!@loc, TacFix (None,n))
+      | "fix"; id = ident; n = natural -> TacAtom (!@loc, TacFix (Some id,n))
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
-	  TacMutualFix (id,n,List.map mk_fix_tac fd)
-      | "cofix" -> TacCofix None
-      | "cofix"; id = ident -> TacCofix (Some id)
+	  TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd))
+      | "cofix" -> TacAtom (!@loc, TacCofix None)
+      | "cofix"; id = ident -> TacAtom (!@loc, TacCofix (Some id))
       | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
-	  TacMutualCofix (id,List.map mk_cofix_tac fd)
+	  TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd))
 
       | IDENT "pose"; (id,b) = bindings_with_parameters ->
-	  TacLetTac (Names.Name id,b,Locusops.nowhere,true,None)
+	  TacAtom (!@loc, TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
       | IDENT "pose"; b = constr; na = as_name ->
-	  TacLetTac (na,b,Locusops.nowhere,true,None)
+	  TacAtom (!@loc, TacLetTac (na,b,Locusops.nowhere,true,None))
       | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
-	  TacLetTac (Names.Name id,c,p,true,None)
+	  TacAtom (!@loc, TacLetTac (Names.Name id,c,p,true,None))
       | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
-          TacLetTac (na,c,p,true,None)
+          TacAtom (!@loc, TacLetTac (na,c,p,true,None))
       | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
           p = clause_dft_all ->
-          TacLetTac (na,c,p,false,e)
+          TacAtom (!@loc, TacLetTac (na,c,p,false,e))
 
       (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAssert (true,None,Some (!@loc,IntroIdentifier id),c)
+	  TacAtom (!@loc, TacAssert (true,None,Some (!@loc,IntroIdentifier id),c))
 
       (* Alternative syntax for "assert c as id by tac" *)
       | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAssert (true,Some tac,Some (!@loc,IntroIdentifier id),c)
+	  TacAtom (!@loc, TacAssert (true,Some tac,Some (!@loc,IntroIdentifier id),c))
 
       (* Alternative syntax for "enough c as id by tac" *)
       | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAssert (false,Some tac,Some (!@loc,IntroIdentifier id),c)
+	  TacAtom (!@loc, TacAssert (false,Some tac,Some (!@loc,IntroIdentifier id),c))
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAssert (true,Some tac,ipat,c)
+	  TacAtom (!@loc, TacAssert (true,Some tac,ipat,c))
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  TacAssert (true,None,ipat,c)
+	  TacAtom (!@loc, TacAssert (true,None,ipat,c))
       | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAssert (false,Some tac,ipat,c)
+	  TacAtom (!@loc, TacAssert (false,Some tac,ipat,c))
 
       | IDENT "generalize"; c = constr ->
-	  TacGeneralize [((AllOccurrences,c),Names.Anonymous)]
+	  TacAtom (!@loc, TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
       | IDENT "generalize"; c = constr; l = LIST1 constr ->
 	  let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
-          TacGeneralize (List.map gen_everywhere (c::l))
+          TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l)))
       | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs;
           na = as_name;
           l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
-          TacGeneralize (((nl,c),na)::l)
-      | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c
+          TacAtom (!@loc, TacGeneralize (((nl,c),na)::l))
+      | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c)
 
       (* Derived basic tactics *)
       | IDENT "induction"; ic = induction_clause_list ->
-	  TacInductionDestruct (true,false,ic)
+	  TacAtom (!@loc, TacInductionDestruct (true,false,ic))
       | IDENT "einduction"; ic = induction_clause_list ->
-	  TacInductionDestruct(true,true,ic)
+	  TacAtom (!@loc, TacInductionDestruct(true,true,ic))
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
-	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
+	  h2 = quantified_hypothesis -> TacAtom (!@loc, TacDoubleInduction (h1,h2))
       | IDENT "destruct"; icl = induction_clause_list ->
-	  TacInductionDestruct(false,false,icl)
+	  TacAtom (!@loc, TacInductionDestruct(false,false,icl))
       | IDENT "edestruct";  icl = induction_clause_list ->
-	  TacInductionDestruct(false,true,icl)
+	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
       | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
-        -> TacDecompose (l,c)
+        -> TacAtom (!@loc, TacDecompose (l,c))
 
       (* Automation tactic *)
-      | d = trivial; lems = auto_using; db = hintbases -> TacTrivial (d,lems,db)
+      | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db))
       | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-          TacAuto (d,n,lems,db)
+          TacAtom (!@loc, TacAuto (d,n,lems,db))
 
       (* Context management *)
-      | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
+      | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
       | IDENT "clear"; l = LIST0 id_or_meta ->
         let is_empty = match l with [] -> true | _ -> false in
-        TacClear (is_empty, l)
-      | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
+        TacAtom (!@loc, TacClear (is_empty, l))
+      | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l)
       | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
-	  TacMove (true,hfrom,hto)
-      | IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
-      | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
+	  TacAtom (!@loc, TacMove (true,hfrom,hto))
+      | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
+      | IDENT "revert"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacRevert l)
 
       (* Constructors *)
-      | "exists"; bll = opt_bindings -> TacSplit (false,bll)
+      | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll))
       | IDENT "eexists"; bll = opt_bindings ->
-	  TacSplit (true,bll)
+	  TacAtom (!@loc, TacSplit (true,bll))
       (* Equivalence relations *)
-      | IDENT "symmetry"; "in"; cl = in_clause -> TacSymmetry cl
+      | IDENT "symmetry"; "in"; cl = in_clause -> TacAtom (!@loc, TacSymmetry cl)
 
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (false,l,cl,t)
+	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
       | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (true,l,cl,t)
+	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
 	  | IDENT "inversion_clear" -> FullInversionClear ];
 	  hyp = quantified_hypothesis;
 	  ids = with_inversion_names; co = OPT ["with"; c = constr -> c] ->
-	    TacInversion (DepInversion (k,co,ids),hyp)
+	    TacAtom (!@loc, TacInversion (DepInversion (k,co,ids),hyp))
       | IDENT "simple"; IDENT "inversion";
 	  hyp = quantified_hypothesis; ids = with_inversion_names;
 	  cl = in_hyp_list ->
-	    TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
+	    TacAtom (!@loc, TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
       | IDENT "inversion";
 	  hyp = quantified_hypothesis; ids = with_inversion_names;
 	  cl = in_hyp_list ->
-	    TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
+	    TacAtom (!@loc, TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
       | IDENT "inversion_clear";
 	  hyp = quantified_hypothesis; ids = with_inversion_names;
 	  cl = in_hyp_list ->
-	    TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
+	    TacAtom (!@loc, TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
       | IDENT "inversion"; hyp = quantified_hypothesis;
 	  "using"; c = constr; cl = in_hyp_list ->
-	    TacInversion (InversionUsing (c,cl), hyp)
+	    TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
 
       (* Conversion *)
-      | r = red_tactic; cl = clause_dft_concl -> TacReduce (r, cl)
+      | r = red_tactic; cl = clause_dft_concl -> TacAtom (!@loc, TacReduce (r, cl))
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
 	  let p,cl = merge_occurrences (!@loc) cl oc in
-	  TacChange (p,c,cl)
+	  TacAtom (!@loc, TacChange (p,c,cl))
     ] ]
   ;
 END;;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 61ca137871..54fcb12b06 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -217,7 +217,7 @@ module Tactic :
     val quantified_hypothesis : quantified_hypothesis Gram.entry
     val int_or_var : int or_var Gram.entry
     val red_expr : raw_red_expr Gram.entry
-    val simple_tactic : raw_atomic_tactic_expr Gram.entry
+    val simple_tactic : raw_tactic_expr Gram.entry
     val simple_intropattern : intro_pattern_expr located Gram.entry
     val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 8ba3319de4..2647ca22af 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -145,9 +145,9 @@ let closed_term_ast l =
   } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
-  TacAtom(Loc.ghost,TacExtend(Loc.ghost,tacname,
+  TacML(Loc.ghost,tacname,
   [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
-   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])))
+   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l]))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 02a21ced6b..c183cb1603 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -654,8 +654,6 @@ let rec pr_atom0 = function
 
   (* Main tactic printer *)
 and pr_atom1 = function
-  | TacExtend (loc,s,l) ->
-      pr_with_comments loc (pr_extend 1 s l)
   | TacAlias (loc,kn,l) ->
       pr_with_comments loc (pr_alias 1 kn (List.map snd l))
 
@@ -938,6 +936,8 @@ let rec pr_tac inherited tac =
          prlist_with_sep spc pr_tacarg l)),
       lcall
   | TacArg (_,a) -> pr_tacarg a, latom
+  | TacML (loc,s,l) ->
+      pr_with_comments loc (pr_extend 1 s l), lcall
   in
   if prec_less prec inherited then strm
   else str"(" ++ strm ++ str")"
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 62b9904d7b..63aea6f432 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -26,7 +26,7 @@ let interp_alias key =
   try KNmap.find key !alias_map
   with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
 
-(** ML tactic extensions (TacExtend) *)
+(** ML tactic extensions (TacML) *)
 
 type ml_tactic =
   typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 4d64a5bb2b..c130ef9132 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -43,7 +43,7 @@ val interp_ltac : KerName.t -> glob_tactic_expr
 
 type ml_tactic =
   typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
-(** Type of external tactics, used by [TacExtend]. *)
+(** Type of external tactics, used by [TacML]. *)
 
 val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit
 (** Register an external tactic. *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 04fd28b309..c9a3d093de 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -559,9 +559,6 @@ let rec intern_atomic lf ist x =
         intern_quantified_hypothesis ist hyp)
 
   (* For extensions *)
-  | TacExtend (loc,opn,l) ->
-      Hook.get f_assert_tactic_installed opn;
-      TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
   | TacAlias (loc,s,l) ->
       let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
       TacAlias (loc,s,l)
@@ -636,6 +633,9 @@ and intern_tactic_seq onlytac ist = function
   | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
   | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
   | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+  | TacML (loc,opn,l) ->
+      let () = Hook.get f_assert_tactic_installed opn in
+      ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l)
 
 and intern_tactic_as_arg loc onlytac ist a =
   match intern_tacarg !strict_check onlytac ist a with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0ae2dc4a7a..a3551760b1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1115,6 +1115,34 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
 	(strbrk "The general \"info\" tactic is currently not working." ++ fnl () ++
 	   strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto.");
       eval_tactic ist tac
+  (* For extensions *)
+  | TacML (loc,opn,l) when List.for_all global_genarg l ->
+      (* spiwack: a special case for tactics (from TACTIC EXTEND) when
+         every argument can be interpreted without a
+         [Proofview.Goal.enter]. *)
+      let tac = Tacenv.interp_ml_tactic opn in
+      (* dummy values, will be ignored *)
+      let env = Environ.empty_env in
+      let sigma = Evd.empty in
+      let concl = Term.mkRel (-1) in
+      let goal = sig_it Goal.V82.dummy_goal in
+      (* /dummy values *)
+      let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in
+      tac args ist
+  | TacML (loc,opn,l) ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let goal_sigma = Proofview.Goal.sigma gl in
+        let concl = Proofview.Goal.concl gl in
+        let goal = Proofview.Goal.goal gl in
+        let tac = Tacenv.interp_ml_tactic opn in
+        let (sigma,args) =
+          Evd.MonadR.List.map_right
+            (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma
+        in
+        Proofview.V82.tclEVARS sigma <*>
+        tac args ist
+      end
 
 and force_vrec ist v : typed_generic_argument GTac.t =
   let v = Value.normalize v in
@@ -1878,34 +1906,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
           hyps
       end
 
-  (* For extensions *)
-  | TacExtend (loc,opn,l) when List.for_all global_genarg l ->
-      (* spiwack: a special case for tactics (from TACTIC EXTEND) when
-         every argument can be interpreted without a
-         [Proofview.Goal.enter]. *)
-      let tac = Tacenv.interp_ml_tactic opn in
-      (* dummy values, will be ignored *)
-      let env = Environ.empty_env in
-      let sigma = Evd.empty in
-      let concl = Term.mkRel (-1) in
-      let goal = sig_it Goal.V82.dummy_goal in
-      (* /dummy values *)
-      let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in
-      tac args ist
-  | TacExtend (loc,opn,l) ->
-      Proofview.Goal.enter begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let goal_sigma = Proofview.Goal.sigma gl in
-        let concl = Proofview.Goal.concl gl in
-        let goal = Proofview.Goal.goal gl in
-        let tac = Tacenv.interp_ml_tactic opn in
-        let (sigma,args) =
-          Evd.MonadR.List.map_right
-            (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma
-        in
-        Proofview.V82.tclEVARS sigma <*>
-        tac args ist
-      end
   | TacAlias (loc,s,l) ->
       let body = Tacenv.interp_alias s in
       let rec f x = match genarg_tag x with
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 93c6edfe65..f2949ab5e8 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -203,8 +203,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp)
 
   (* For extensions *)
-  | TacExtend (_loc,opn,l) ->
-      TacExtend (dloc,opn,List.map (subst_genarg subst) l)
   | TacAlias (_,s,l) ->
       let s = subst_kn subst s in
       TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
@@ -253,6 +251,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
   | TacComplete tac -> TacComplete (subst_tactic subst tac)
   | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a)
+  | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_genarg subst) l)
 
 and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4f0bc58482..d972fb9294 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -156,7 +156,7 @@ let flatten_contravariant_conj flags ist =
 let constructor i =
   let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
   let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
-  Tacexpr.TacAtom (Loc.ghost, Tacexpr.TacExtend (Loc.ghost, name, [i]))
+  Tacexpr.TacML (Loc.ghost, name, [i])
 
 let is_disj flags ist =
   let t = assoc_var "X1" ist in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4e3d460ded..e40e8a73a9 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1196,7 +1196,7 @@ let explain_ltac_call_trace last trace loc =
 let skip_extensions trace =
   let rec aux = function
   | (_,Proof_type.LtacAtomCall
-      (Tacexpr.TacAlias _ | Tacexpr.TacExtend _) as tac) :: tail -> [tac]
+      (Tacexpr.TacAlias _) as tac) :: tail -> [tac]
   | _ :: tail -> aux tail
   | [] -> [] in
   List.rev (aux (List.rev trace))
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fb1e0391b5..00733d5eec 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -140,8 +140,7 @@ let extend_atomic_tactic name entries =
   let add_atomic (id, args) = match args with
   | None -> ()
   | Some args ->
-    let loc = Loc.ghost in
-    let body = Tacexpr.TacAtom (loc, Tacexpr.TacExtend (loc, name, args)) in
+    let body = Tacexpr.TacML (Loc.ghost, name, args) in
     Tacenv.register_atomic_ltac (Names.Id.of_string id) body
   in
   List.iter add_atomic entries