aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tacenv.ml2
-rw-r--r--tactics/tacenv.mli2
-rw-r--r--tactics/tacintern.ml6
-rw-r--r--tactics/tacinterp.ml56
-rw-r--r--tactics/tacsubst.ml3
-rw-r--r--tactics/tauto.ml42
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-17 20:52:22 +0000