aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tactics.ml9
-rw-r--r--tactics/tactics.mli6
7 files changed, 17 insertions, 24 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5b9f82aa5..f57f12f66 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -706,7 +706,7 @@ let build_proof
in
tclTHENSEQ
[
- Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+ generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
thin dyn_infos.rec_hyps;
pattern_option [Locus.AllOccurrencesBut [1],t] None;
(fun g -> observe_tac "toto" (
@@ -933,7 +933,7 @@ let generalize_non_dep hyp g =
in
(* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
tclTHEN
- ((* observe_tac "h_generalize" *) (Simple.generalize (List.map mkVar to_revert) ))
+ ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) ))
((* observe_tac "thin" *) (thin to_revert))
g
@@ -1563,7 +1563,7 @@ let prove_principle_for_gen
Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
in
let revert l =
- tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l)
+ tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
in
let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 363dd1b3b..628e582e2 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -458,7 +458,7 @@ let generalize_dependent_of x hyp g =
tclMAP
(function
| (id,None,t) when not (Id.equal id hyp) &&
- (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id])
+ (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id])
| _ -> tclIDTAC
)
(pf_hyps g)
@@ -699,7 +699,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
})
Locusops.onConcl
;
- Simple.generalize (List.map mkVar ids);
+ generalize (List.map mkVar ids);
thin ids
]
else
@@ -738,7 +738,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
tclTHENSEQ
[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
observe_tac "h_generalize"
- (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+ (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
Proofview.V82.of_tactic (Simple.intro graph_principle_id);
observe_tac "" (tclTHEN_i
(observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
@@ -921,7 +921,7 @@ let revert_graph kn post_tac hid g =
let f_args,res = Array.chop (Array.length args - 1) args in
tclTHENSEQ
[
- Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+ generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
post_tac hid
@@ -965,7 +965,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
in
tclTHENSEQ[
pre_tac hid;
- Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+ generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6867939c2..60ff10922 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -687,7 +687,7 @@ let mkDestructEq :
to_revert_constr in
pf_typel new_hyps (fun _ ->
observe_tclTHENLIST (str "mkDestructEq")
- [Simple.generalize new_hyps;
+ [generalize new_hyps;
(fun g2 ->
let changefun patvars = { run = fun sigma ->
let sigma = Sigma.to_evar_map sigma in
@@ -1115,7 +1115,7 @@ let termination_proof_header is_mes input_type ids args_id relation
[observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
- tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id]))
+ tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))
))
;
observe_tac (str "fix") (fix (Some hrec) (nargs+1));
@@ -1305,7 +1305,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
observe_tclTHENLIST (str "")
[
- Simple.generalize [lemma];
+ generalize [lemma];
Proofview.V82.of_tactic (Simple.intro hid);
(fun g ->
let ids = pf_ids_of_hyps g in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0f907b0ef..8a4b20601 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -716,7 +716,7 @@ let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
Tacticals.New.tclTHENLIST
- [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+ [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 850580f75..bfe3097e2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1932,7 +1932,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclWITHHOLES false
(name_atomic ~env
(TacGeneralize cl)
- (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma
+ (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
end }
| TacGeneralizeDep c ->
(new_interp_constr ist c) (fun c ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c76aeb4a8..539c2ab71 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2647,7 +2647,8 @@ let new_generalize_gen_let lconstr =
end }
let generalize_gen lconstr =
- generalize_gen_let (List.map (fun ((occs,c),na) ->
+ generalize_gen_let (List.map (fun (occs_c,na) ->
+ let (occs,c) = Redexpr.out_with_occurrences occs_c in
(occs,c,None),na) lconstr)
let new_generalize_gen lconstr =
@@ -4652,12 +4653,6 @@ module Simple = struct
let intro x = intro_move (Some x) MoveLast
- let generalize_gen cl =
- generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)
- let generalize cl =
- generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
- cl)
-
let apply c =
apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))]
let eapply c =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 129837d08..f06a50f79 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -385,7 +385,8 @@ val letin_pat_tac : (bool * intro_pattern_naming) option ->
(** {6 Generalize tactics. } *)
val generalize : constr list -> tactic
-val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic
+val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic
+
val new_generalize : constr list -> unit Proofview.tactic
val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic
@@ -417,9 +418,6 @@ module Simple : sig
(** Simplified version of some of the above tactics *)
val intro : Id.t -> unit Proofview.tactic
- val generalize : constr list -> tactic
- val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic
-
val apply : constr -> unit Proofview.tactic
val eapply : constr -> unit Proofview.tactic
val elim : constr -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 07:53:56 +0000