diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 7 | ||||
| -rw-r--r-- | proofs/refiner.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.mli | 11 | ||||
| -rw-r--r-- | tactics/auto.ml | 16 | ||||
| -rw-r--r-- | tactics/elim.ml | 12 | ||||
| -rw-r--r-- | tactics/eqdecide.ml4 | 6 | ||||
| -rw-r--r-- | tactics/hiddentac.ml | 98 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 14 |
9 files changed, 61 insertions, 111 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 8b5b64ffc2..5500a233a3 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -174,12 +174,7 @@ let declare_tactic loc s cl = let hide_tac (p,e) = (* reste a definir les fonctions cachees avec des noms frais *) let stac = "h_"^s in - let e = - make_fun - <:expr< - Refiner.abstract_extended_tactic $make_eval_tactic e p$ - >> - p in + let e = make_fun (make_eval_tactic e p) p in <:str_item< value $lid:stac$ = $e$ >> in let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 33b070e765..5bc3161b93 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -23,10 +23,6 @@ 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 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 {it=sgl; sigma = sigma'} diff --git a/proofs/refiner.mli b/proofs/refiner.mli index bc47a73c9f..d353a566fa 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -26,17 +26,6 @@ val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list -(** {6 Hiding the implementation of tactics. } *) - -(** [abstract_tactic tac] hides the (partial) proof produced by [tac] under - a single proof node. The boolean tells if the default tactic is used. *) -(* spiwack: currently here for compatibility, the tactic expression - is discarded and we simply return the tactic. *) - -val abstract_tactic : tactic -> tactic -val abstract_tactic_expr : tactic -> tactic -val abstract_extended_tactic : tactic -> tactic - val refiner : rule -> tactic (** {6 Tacticals. } *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 926e65d29a..d773d20923 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1016,19 +1016,15 @@ let auto_unif_flags = { (* Try unification with the precompiled clause, then use registered Apply *) -let h_clenv_refine ev c clenv = - Refiner.abstract_tactic - (Clenvtac.clenv_refine ev clenv) - let unify_resolve_nodelta (c,clenv) gl = let clenv' = connect_clenv gl clenv in let clenv'' = clenv_unique_resolver ~flags:auto_unif_flags clenv' gl in - h_clenv_refine false c clenv'' gl + Clenvtac.clenv_refine false clenv'' gl let unify_resolve flags (c,clenv) gl = let clenv' = connect_clenv gl clenv in let clenv'' = clenv_unique_resolver ~flags clenv' gl in - h_clenv_refine false c clenv'' gl + Clenvtac.clenv_refine false clenv'' gl let unify_resolve_gen = function | None -> unify_resolve_nodelta @@ -1354,9 +1350,7 @@ let gen_trivial ?(debug=Off) lems = function | None -> full_trivial ~debug lems | Some l -> trivial ~debug lems l -let h_trivial ?(debug=Off) lems l = - Refiner.abstract_tactic - (gen_trivial ~debug lems l) +let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l (**************************************************************************) (* The classical Auto tactic *) @@ -1438,6 +1432,4 @@ 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 - (gen_auto ~debug n lems l) +let h_auto ?(debug=Off) n lems l = gen_auto ~debug n lems l diff --git a/tactics/elim.ml b/tactics/elim.ml index a25a370922..685a70badb 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -122,14 +122,11 @@ let decompose_or c gls = (fun (_,t) -> is_disjunction t) c gls -let h_decompose l c = - Refiner.abstract_tactic (decompose_these c l) +let h_decompose l c = decompose_these c l -let h_decompose_or c = - Refiner.abstract_tactic (decompose_or c) +let h_decompose_or = decompose_or -let h_decompose_and c = - Refiner.abstract_tactic (decompose_and c) +let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) @@ -174,7 +171,6 @@ let double_ind h1 h2 gls = (introElimAssumsThen (induction_trailer abs_i abs_j)) ([],[]) (mkVar id)))) gls -let h_double_induction h1 h2 = - Refiner.abstract_tactic (double_ind h1 h2) +let h_double_induction = double_ind diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 89d2a85d8b..df85e564eb 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -72,10 +72,6 @@ let solveNoteqBranch side = (tclTHEN introf (onLastHypId (fun id -> Extratactics.h_discrHyp id))) -let h_solveNoteqBranch side = - Refiner.abstract_extended_tactic - (solveNoteqBranch side) - (* Constructs the type {c1=c2}+{~c1=c2} *) let mkDecideEqGoal eqonleft op rectype c1 c2 g = @@ -151,7 +147,7 @@ let decideGralEquality g = in (tclTHEN (mkBranches c1 c2) - (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype))) + (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) g with PatternMatchingFailure -> error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}." diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 25106d1ef9..57326a485d 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -14,97 +14,85 @@ open Locus open Misctypes (* Basic tactics *) -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 (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) = - 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_intro_move = intro_move +let h_intro x = h_intro_move (Some x) MoveLast +let h_intros_until = intros_until +let h_assumption = assumption +let h_exact = exact_check +let h_exact_no_check = exact_no_check +let h_vm_cast_no_check = vm_cast_no_check +let h_apply = apply_with_bindings_gen +let h_apply_in simple ev cb (id,ipat) = apply_in simple ev id cb ipat +let h_elim = elim +let h_elim_type = elim_type +let h_case = general_case_analysis +let h_case_type = case_type +let h_fix = fix +let h_mutual_fix b id n l = mutual_fix id n 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_cofix = cofix +let h_mutual_cofix b id l = mutual_cofix id l 0 -let h_cut c = abstract_tactic (cut c) +let h_cut = cut let h_generalize_gen cl = - abstract_tactic - (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) + 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 (generalize_dep c) +let h_generalize_dep = generalize_dep 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 (letin_tac with_eq na c None cl) + 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 (letin_pat_tac with_eq na c None cl) + letin_pat_tac with_eq na c None cl (* Derived basic tactics *) let h_simple_induction_destruct isrec h = - abstract_tactic (if isrec then (simple_induct h) else (simple_destruct h)) + 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 h_induction_destruct isrec ev lcl = - abstract_tactic (induction_destruct isrec ev lcl) +let h_induction_destruct = induction_destruct 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 (specialize n d) -let h_lapply c = abstract_tactic (cut_and_apply c) +let h_specialize = specialize +let h_lapply = cut_and_apply (* Context management *) -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) +let h_clear b l = (if b then keep else clear) l +let h_clear_body = clear_body +let h_move = move_hyp +let h_rename = rename_hyp +let h_revert = revert (* Constructors *) -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 (constructor_tac ev None n l) -let h_one_constructor n = - abstract_tactic (one_constructor n NoBindings) +let h_left = left_with_bindings +let h_right = right_with_bindings +let h_split = split_with_bindings + +let h_constructor ev n l = constructor_tac ev None n l +let h_one_constructor n = 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 (reduce r cl) -let h_change op c cl = - abstract_tactic (change op c cl) +let h_reduce = reduce +let h_change = change (* Equivalence relations *) -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_reflexivity = intros_reflexivity +let h_symmetry = intros_symmetry +let h_transitivity = intros_transitivity 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 (intro_patterns l) +let h_intro_patterns = intro_patterns diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 7437ab56f4..f7426c8f10 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -20,7 +20,7 @@ open Clenv open Termops open Misctypes -(** Tactics for the interpreter. They left a trace in the proof tree +(** Tactics for the interpreter. They used to left a trace in the proof tree when they are called. *) (** Basic tactics *) @@ -56,7 +56,7 @@ val h_cofix : identifier option -> tactic val h_cut : constr -> tactic val h_generalize : constr list -> tactic val h_generalize_gen : (constr Locus.with_occurrences * name) list -> tactic -val h_generalize_dep : constr -> tactic +val h_generalize_dep : ?with_let:bool -> constr -> tactic val h_let_tac : letin_flag -> name -> constr -> Locus.clause -> intro_pattern_expr located option -> tactic val h_let_pat_tac : letin_flag -> name -> evar_map * constr -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 215dee8377..35da9ee98a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2394,9 +2394,8 @@ 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 - (Tactics.forward (Option.map (interp_tactic ist) t) - (Option.map (interp_intro_pattern ist gl) ipat) c)) + (Tactics.forward (Option.map (interp_tactic ist) t) + (Option.map (interp_intro_pattern ist gl) ipat) c) | TacGeneralize cl -> let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in tclWITHHOLES false (h_generalize_gen) sigma cl @@ -2493,8 +2492,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 - (Tactics.any_constructor ev (Option.map (interp_tactic ist) t)) + Tactics.any_constructor ev (Option.map (interp_tactic ist) t) | TacConstructor (ev,n,bl) -> let sigma, bl = interp_bindings ist env sigma bl in tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl @@ -2583,7 +2581,7 @@ and interp_atomic ist gl tac = sigma , a_interp::acc end l (project gl,[]) in - abstract_extended_tactic (tac args) + tac args | TacAlias (loc,s,l,(_,body)) -> fun gl -> let evdref = ref gl.sigma in let f x = match genarg_tag x with @@ -2727,8 +2725,8 @@ let hide_interp t ot gl = let te = intern_tactic true ist t in let t = eval_tactic te in match ot with - | None -> abstract_tactic_expr t gl - | Some t' -> abstract_tactic_expr (tclTHEN t t') gl + | None -> t gl + | Some t' -> (tclTHEN t t') gl (***************************************************************************) (* Substitution at module closing time *) |