aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml46
-rw-r--r--intf/tacexpr.mli5
-rw-r--r--parsing/egramcoq.ml20
-rw-r--r--parsing/egramcoq.mli2
-rw-r--r--parsing/g_ltac.ml42
-rw-r--r--parsing/g_tactic.ml4122
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--printing/pptactic.ml4
-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
-rw-r--r--toplevel/himsg.ml2
-rw-r--r--toplevel/metasyntax.ml3
17 files changed, 117 insertions, 126 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 9631ed95e..312f0e949 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 8e5b51b87..b9c41ae03 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 e8072aa1a..c56a5a700 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 2a5e89eb9..4cb55ee8e 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 ea3835866..ce3105548 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 a29c782c5..2f9ab38d2 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 61ca13787..54fcb12b0 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 8ba3319de..2647ca22a 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 02a21ced6..c183cb160 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 62b9904d7..63aea6f43 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 4d64a5bb2..c130ef913 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 04fd28b30..c9a3d093d 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 0ae2dc4a7..a3551760b 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 93c6edfe6..f2949ab5e 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 4f0bc5848..d972fb929 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 4e3d460de..e40e8a73a 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 fb1e0391b..00733d5ee 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 07:45:07 +0000