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.

6 files changed, 35 insertions, 36 deletions

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