aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml42
-rw-r--r--plugins/xml/dumptree.ml49
-rw-r--r--printing/pptactic.ml15
-rw-r--r--printing/pptactic.mli2
-rw-r--r--proofs/proof_type.ml33
-rw-r--r--proofs/proof_type.mli34
-rw-r--r--proofs/refiner.ml6
-rw-r--r--proofs/refiner.mli7
-rw-r--r--tactics/auto.ml6
-rw-r--r--tactics/elim.ml8
-rw-r--r--tactics/eqdecide.ml42
-rw-r--r--tactics/hiddentac.ml112
-rw-r--r--tactics/tacinterp.ml13
13 files changed, 63 insertions, 186 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index f11927e77..8b5b64ffc 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -177,7 +177,7 @@ let declare_tactic loc s cl =
let e =
make_fun
<:expr<
- Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$
+ Refiner.abstract_extended_tactic $make_eval_tactic e p$
>>
p in
<:str_item< value $lid:stac$ = $e$ >>
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index c0c8ada95..1fd829e7a 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -36,15 +36,6 @@ let thin_sign osign sign =
sign ~init:Environ.empty_named_context_val
;;
-let pr_tactic_xml = function
- | TacArg (_,Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>"
- | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>"
-;;
-
-let pr_proof_instr_xml instr =
- Ppdecl_proof.pr_proof_instr (Global.env()) instr
-;;
-
let pr_var_decl_xml env (id,c,typ) =
let ptyp = print_constr_env env typ in
match c with
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b790c4ea6..055f08d93 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1035,23 +1035,8 @@ and pr_glob_tactic_level env n (t:glob_tactic_expr) =
let pr_constr_or_lconstr_pattern b =
if b then pr_lconstr_pattern else pr_constr_pattern
-let typed_printers =
- (pr_glob_tactic_level,
- pr_constr_env,
- pr_lconstr_env,
- pr_constr_or_lconstr_pattern,
- pr_evaluable_reference_env,
- pr_inductive,
- pr_ltac_constant,
- pr_id,
- pr_extend,
- strip_prod_binders_constr)
-
-let pr_tactic_level env = fst (make_pr_tac typed_printers env)
-
let pr_raw_tactic env = pr_raw_tactic_level env ltop
let pr_glob_tactic env = pr_glob_tactic_level env ltop
-let pr_tactic env = pr_tactic_level env ltop
let _ = Tactic_debug.set_tactic_printer
(fun x -> pr_glob_tactic (Global.env()) x)
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 61acffd08..8973bd6bc 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -92,8 +92,6 @@ val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
-val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds
-
val pr_hintbases : string list option -> std_ppcmds
val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index b84b6db48..e09d72e47 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -46,39 +46,6 @@ type prim_rule =
type rule = prim_rule
-type tactic_expr =
- (constr,
- constr_pattern,
- evaluable_global_reference,
- inductive,
- ltac_constant,
- identifier,
- glob_tactic_expr,
- tlevel)
- Tacexpr.gen_tactic_expr
-
-and atomic_tactic_expr =
- (constr,
- constr_pattern,
- evaluable_global_reference,
- inductive,
- ltac_constant,
- identifier,
- glob_tactic_expr,
- tlevel)
- Tacexpr.gen_atomic_tactic_expr
-
-and tactic_arg =
- (constr,
- constr_pattern,
- evaluable_global_reference,
- inductive,
- ltac_constant,
- identifier,
- glob_tactic_expr,
- tlevel)
- Tacexpr.gen_tactic_arg
-
(** Ltac traces *)
type ltac_call_kind =
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 6688d6e62..95ca33e90 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -70,40 +70,6 @@ type goal = Goal.goal
type tactic = goal sigma -> goal list sigma
-
-type tactic_expr =
- (constr,
- constr_pattern,
- evaluable_global_reference,
- inductive,
- ltac_constant,
- identifier,
- glob_tactic_expr,
- tlevel)
- Tacexpr.gen_tactic_expr
-
-and atomic_tactic_expr =
- (constr,
- constr_pattern,
- evaluable_global_reference,
- inductive,
- ltac_constant,
- identifier,
- glob_tactic_expr,
- tlevel)
- Tacexpr.gen_atomic_tactic_expr
-
-and tactic_arg =
- (constr,
- constr_pattern,
- evaluable_global_reference,
- inductive,
- ltac_constant,
- identifier,
- glob_tactic_expr,
- tlevel)
- Tacexpr.gen_tactic_arg
-
(** Ltac traces *)
type ltac_call_kind =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 4b5bdcfe9..33b070e76 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -23,9 +23,9 @@ let project x = x.sigma
let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
-let abstract_tactic_expr ?(dflt=false) te tacfun = tacfun
-let abstract_tactic ?(dflt=false) te tacfun = tacfun
-let abstract_extended_tactic ?(dflt=false) s args tacfun = tacfun
+let abstract_tactic_expr tacfun = tacfun
+let abstract_tactic tacfun = tacfun
+let abstract_extended_tactic tacfun = tacfun
let refiner pr goal_sigma =
let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 6f11e7115..bc47a73c9 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -33,10 +33,9 @@ val apply_sig_tac :
(* spiwack: currently here for compatibility, the tactic expression
is discarded and we simply return the tactic. *)
-val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
-val abstract_extended_tactic :
- ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
+val abstract_tactic : tactic -> tactic
+val abstract_tactic_expr : tactic -> tactic
+val abstract_extended_tactic : tactic -> tactic
val refiner : rule -> tactic
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 748b608b4..926e65d29 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1017,7 +1017,7 @@ let auto_unif_flags = {
(* Try unification with the precompiled clause, then use registered Apply *)
let h_clenv_refine ev c clenv =
- Refiner.abstract_tactic (TacApply (true,ev,[c,NoBindings],None))
+ Refiner.abstract_tactic
(Clenvtac.clenv_refine ev clenv)
let unify_resolve_nodelta (c,clenv) gl =
@@ -1355,7 +1355,7 @@ let gen_trivial ?(debug=Off) lems = function
| Some l -> trivial ~debug lems l
let h_trivial ?(debug=Off) lems l =
- Refiner.abstract_tactic (TacTrivial (debug,List.map snd lems,l))
+ Refiner.abstract_tactic
(gen_trivial ~debug lems l)
(**************************************************************************)
@@ -1439,5 +1439,5 @@ let gen_auto ?(debug=Off) n lems dbnames =
let inj_or_var = Option.map (fun n -> ArgArg n)
let h_auto ?(debug=Off) n lems l =
- Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
+ Refiner.abstract_tactic
(gen_auto ~debug n lems l)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 32acc5af5..a25a37092 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -123,13 +123,13 @@ let decompose_or c gls =
c gls
let h_decompose l c =
- Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l)
+ Refiner.abstract_tactic (decompose_these c l)
let h_decompose_or c =
- Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c)
+ Refiner.abstract_tactic (decompose_or c)
let h_decompose_and c =
- Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c)
+ Refiner.abstract_tactic (decompose_and c)
(* The tactic Double performs a double induction *)
@@ -175,6 +175,6 @@ let double_ind h1 h2 gls =
([],[]) (mkVar id)))) gls
let h_double_induction h1 h2 =
- Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2)
+ Refiner.abstract_tactic (double_ind h1 h2)
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 5329029a8..89d2a85d8 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -73,7 +73,7 @@ let solveNoteqBranch side =
(onLastHypId (fun id -> Extratactics.h_discrHyp id)))
let h_solveNoteqBranch side =
- Refiner.abstract_extended_tactic "solveNoteqBranch" []
+ Refiner.abstract_extended_tactic
(solveNoteqBranch side)
(* Constructs the type {c1=c2}+{~c1=c2} *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b68b6c545..25106d1ef 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -14,125 +14,97 @@ open Locus
open Misctypes
(* Basic tactics *)
-let h_intro_move x y =
- abstract_tactic (TacIntroMove (x, y)) (intro_move x y)
+let h_intro_move x y = abstract_tactic (intro_move x y)
let h_intro x = h_intro_move (Some x) MoveLast
-let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
-let h_assumption = abstract_tactic TacAssumption assumption
-let h_exact c = abstract_tactic (TacExact c) (exact_check c)
-let h_exact_no_check c =
- abstract_tactic (TacExactNoCheck c) (exact_no_check c)
-let h_vm_cast_no_check c =
- abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c)
-let h_apply simple ev cb =
- abstract_tactic (TacApply (simple,ev,List.map snd cb,None))
+let h_intros_until x = abstract_tactic (intros_until x)
+let h_assumption = abstract_tactic assumption
+let h_exact c = abstract_tactic (exact_check c)
+let h_exact_no_check c = abstract_tactic (exact_no_check c)
+let h_vm_cast_no_check c = abstract_tactic (vm_cast_no_check c)
+let h_apply simple ev cb = abstract_tactic
(apply_with_bindings_gen simple ev cb)
-let h_apply_in simple ev cb (id,ipat as inhyp) =
- abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp))
- (apply_in simple ev id cb ipat)
-let h_elim ev cb cbo =
- abstract_tactic (TacElim (ev,cb,cbo))
- (elim ev cb cbo)
-let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c)
-let h_case ev cb = abstract_tactic (TacCase (ev,cb)) (general_case_analysis ev cb)
-let h_case_type c = abstract_tactic (TacCaseType c) (case_type c)
-let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n)
-let h_mutual_fix b id n l =
- abstract_tactic
- (TacMutualFix (b,id,n,l))
- (mutual_fix id n l 0)
+let h_apply_in simple ev cb (id,ipat) =
+ abstract_tactic (apply_in simple ev id cb ipat)
+let h_elim ev cb cbo = abstract_tactic (elim ev cb cbo)
+let h_elim_type c = abstract_tactic (elim_type c)
+let h_case ev cb = abstract_tactic (general_case_analysis ev cb)
+let h_case_type c = abstract_tactic (case_type c)
+let h_fix ido n = abstract_tactic (fix ido n)
+let h_mutual_fix b id n l = abstract_tactic (mutual_fix id n l 0)
-let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido)
-let h_mutual_cofix b id l =
- abstract_tactic
- (TacMutualCofix (b,id,l))
- (mutual_cofix id l 0)
+let h_cofix ido = abstract_tactic (cofix ido)
+let h_mutual_cofix b id l = abstract_tactic (mutual_cofix id l 0)
-let h_cut c = abstract_tactic (TacCut c) (cut c)
+let h_cut c = abstract_tactic (cut c)
let h_generalize_gen cl =
- abstract_tactic (TacGeneralize cl)
+ abstract_tactic
(generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl))
let h_generalize cl =
h_generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
cl)
let h_generalize_dep c =
- abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
+ abstract_tactic (generalize_dep c)
let h_let_tac b na c cl eqpat =
let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
- abstract_tactic (TacLetTac (na,c,cl,b,eqpat))
- (letin_tac with_eq na c None cl)
+ abstract_tactic (letin_tac with_eq na c None cl)
let h_let_pat_tac b na c cl eqpat =
let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
- abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat))
- (letin_pat_tac with_eq na c None cl)
+ abstract_tactic (letin_pat_tac with_eq na c None cl)
(* Derived basic tactics *)
let h_simple_induction_destruct isrec h =
- abstract_tactic (TacSimpleInductionDestruct (isrec,h))
- (if isrec then (simple_induct h) else (simple_destruct h))
+ abstract_tactic (if isrec then (simple_induct h) else (simple_destruct h))
let h_simple_induction = h_simple_induction_destruct true
let h_simple_destruct = h_simple_induction_destruct false
-let out_indarg = function
- | ElimOnConstr (_,c) -> ElimOnConstr c
- | ElimOnIdent id -> ElimOnIdent id
- | ElimOnAnonHyp n -> ElimOnAnonHyp n
-
let h_induction_destruct isrec ev lcl =
- let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in
- abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
- (induction_destruct isrec ev lcl)
+ abstract_tactic (induction_destruct isrec ev lcl)
let h_new_induction ev c idl e cl =
h_induction_destruct true ev ([c,idl],e,cl)
let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
-let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
-let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
+let h_specialize n d = abstract_tactic (specialize n d)
+let h_lapply c = abstract_tactic (cut_and_apply c)
(* Context management *)
-let h_clear b l = abstract_tactic (TacClear (b,l))
- ((if b then keep else clear) l)
-let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l)
-let h_move dep id1 id2 =
- abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
-let h_rename l =
- abstract_tactic (TacRename l) (rename_hyp l)
-let h_revert l = abstract_tactic (TacRevert l) (revert l)
+let h_clear b l = abstract_tactic ((if b then keep else clear) l)
+let h_clear_body l = abstract_tactic (clear_body l)
+let h_move dep id1 id2 = abstract_tactic (move_hyp dep id1 id2)
+let h_rename l = abstract_tactic (rename_hyp l)
+let h_revert l = abstract_tactic (revert l)
(* Constructors *)
-let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_bindings ev l)
-let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_bindings ev l)
-let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_bindings ev l)
+let h_left ev l = abstract_tactic (left_with_bindings ev l)
+let h_right ev l = abstract_tactic (right_with_bindings ev l)
+let h_split ev l = abstract_tactic (split_with_bindings ev l)
(* Moved to tacinterp because of dependencies in Tacinterp.interp
let h_any_constructor t =
abstract_tactic (TacAnyConstructor t) (any_constructor t)
*)
let h_constructor ev n l =
- abstract_tactic (TacConstructor(ev,ArgArg n,l))(constructor_tac ev None n l)
+ abstract_tactic (constructor_tac ev None n l)
let h_one_constructor n =
- abstract_tactic (TacConstructor(false,ArgArg n,NoBindings)) (one_constructor n NoBindings)
+ abstract_tactic (one_constructor n NoBindings)
let h_simplest_left = h_left false NoBindings
let h_simplest_right = h_right false NoBindings
(* Conversion *)
let h_reduce r cl =
- abstract_tactic (TacReduce (r,cl)) (reduce r cl)
+ abstract_tactic (reduce r cl)
let h_change op c cl =
- abstract_tactic (TacChange (op,c,cl)) (change op c cl)
+ abstract_tactic (change op c cl)
(* Equivalence relations *)
-let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity
-let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c)
-let h_transitivity c =
- abstract_tactic (TacTransitivity c)
- (intros_transitivity c)
+let h_reflexivity = abstract_tactic intros_reflexivity
+let h_symmetry c = abstract_tactic (intros_symmetry c)
+let h_transitivity c = abstract_tactic (intros_transitivity c)
let h_simplest_apply c = h_apply false false [Loc.ghost,(c,NoBindings)]
let h_simplest_eapply c = h_apply false true [Loc.ghost,(c,NoBindings)]
let h_simplest_elim c = h_elim false (c,NoBindings) None
let h_simplest_case c = h_case false (c,NoBindings)
-let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l)
+let h_intro_patterns l = abstract_tactic (intro_patterns l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 12c970d68..2ed054ea1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2380,7 +2380,7 @@ and interp_atomic ist gl tac =
let (sigma,c) = (if t=None then interp_constr else interp_type) ist env sigma c in
tclTHEN
(tclEVARS sigma)
- (abstract_tactic (TacAssert (t,ipat,c))
+ (abstract_tactic
(Tactics.forward (Option.map (interp_tactic ist) t)
(Option.map (interp_intro_pattern ist gl) ipat) c))
| TacGeneralize cl ->
@@ -2479,7 +2479,7 @@ and interp_atomic ist gl tac =
let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
tclWITHHOLES ev (h_split ev) sigma bll
| TacAnyConstructor (ev,t) ->
- abstract_tactic (TacAnyConstructor (ev,t))
+ abstract_tactic
(Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
| TacConstructor (ev,n,bl) ->
let sigma, bl = interp_bindings ist env sigma bl in
@@ -2569,7 +2569,7 @@ and interp_atomic ist gl tac =
sigma , a_interp::acc
end l (project gl,[])
in
- abstract_extended_tactic opn args (tac args)
+ abstract_extended_tactic (tac args)
| TacAlias (loc,s,l,(_,body)) -> fun gl ->
let evdref = ref gl.sigma in
let f x = match genarg_tag x with
@@ -2706,16 +2706,15 @@ let eval_ltac_constr gl t =
{ lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl
(intern_tactic_or_tacarg (make_empty_glob_sign ()) t )
-(* Hides interpretation for pretty-print *)
+(* Used to hide interpretation for pretty-print, now just launch tactics *)
let hide_interp t ot gl =
let ist = { ltacvars = ([],[]); ltacrecvars = [];
gsigma = project gl; genv = pf_env gl } in
let te = intern_tactic true ist t in
let t = eval_tactic te in
match ot with
- | None -> abstract_tactic_expr (TacArg (dloc,Tacexp te)) t gl
- | Some t' ->
- abstract_tactic_expr ~dflt:true (TacArg (dloc,Tacexp te)) (tclTHEN t t') gl
+ | None -> abstract_tactic_expr t gl
+ | Some t' -> abstract_tactic_expr (tclTHEN t t') gl
(***************************************************************************)
(* Substitution at module closing time *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 07:13:21 +0000