aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ltac/extratactics.ml42
-rw-r--r--ltac/tacinterp.ml2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml6
-rw-r--r--plugins/firstorder/instances.ml8
-rw-r--r--plugins/firstorder/rules.ml8
-rw-r--r--plugins/funind/functional_principles_proofs.ml10
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--plugins/micromega/coq_micromega.ml8
-rw-r--r--plugins/nsatz/g_nsatz.ml42
-rw-r--r--plugins/omega/coq_omega.ml58
-rw-r--r--plugins/romega/refl_omega.ml4
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/tactics.ml18
-rw-r--r--tactics/tactics.mli5
15 files changed, 73 insertions, 76 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 1f3eb1335..e03cc675e 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -728,7 +728,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.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+ [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/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5aff262aa..7ec1b2ca0 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclWITHHOLES false
(name_atomic ~env
(TacGeneralize cl)
- (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
+ (Tactics.generalize_gen cl)) sigma
end }
| TacLetTac (na,c,clp,b,eqpat) ->
Proofview.V82.nf_evar_goals <*>
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a6b338164..de06af005 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1289,7 +1289,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
(fun id ->
hrec_for (out_name fix_name) per_info gls1 id)
recs in
- generalize hrecs gls1
+ Proofview.V82.of_tactic (generalize hrecs) gls1
end;
match bro with
None ->
@@ -1365,7 +1365,7 @@ let end_tac et2 gls =
(default_justification (List.map mkVar clauses))
| ET_Induction,EK_nodep ->
tclTHENLIST
- [generalize (pi.per_args@[pi.per_casee]);
+ [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]));
Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
default_justification (List.map mkVar clauses)]
| ET_Case_analysis,EK_dep tree ->
@@ -1377,7 +1377,7 @@ let end_tac et2 gls =
(initial_instance_stack clauses) [pi.per_casee] 0 tree
| ET_Induction,EK_dep tree ->
let nargs = (List.length pi.per_args) in
- tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+ tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])))
begin
fun gls0 ->
let fix_id =
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 0e2a40245..5eff2f277 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -135,9 +135,9 @@ let left_instance_tac (inst,id) continue seq=
[tclTHENLIST
[Proofview.V82.of_tactic introf;
pf_constr_of_global id (fun idc ->
- (fun gls->generalize
+ (fun gls-> Proofview.V82.of_tactic (generalize
[mkApp(idc,
- [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
+ [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
Proofview.V82.of_tactic introf;
tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
@@ -158,10 +158,10 @@ let left_instance_tac (inst,id) continue seq=
try Typing.type_of (pf_env gl) evmap gt
with e when Errors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
- tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
+ tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
else
pf_constr_of_global id (fun idc ->
- generalize [mkApp(idc,[|t|])])
+ Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
in
tclTHENLIST
[special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index d05e9484a..92b6e828e 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -67,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq=
tclTHENLIST
[pf_constr_of_global (find_left a seq) (fun left ->
pf_constr_of_global id (fun id ->
- generalize [mkApp(id, [|left|])]));
+ Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
clear_global id;
Proofview.V82.of_tactic intro]
with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -135,7 +135,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
let newhyps idc =List.init lp (myterm idc) in
tclIFTHENELSE
(tclTHENLIST
- [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
+ [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
clear_global id;
tclDO lp (Proofview.V82.of_tactic intro)])
(wrap lp false continue seq) backtrack gl
@@ -153,7 +153,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
tclTHENS (Proofview.V82.of_tactic (cut cc))
[pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
tclTHENLIST
- [pf_constr_of_global id (fun idc -> generalize [d idc]);
+ [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
clear_global id;
Proofview.V82.of_tactic introf;
Proofview.V82.of_tactic introf;
@@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq=
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
let term=mkApp(idc,[|mkVar(id0)|]) in
- tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls));
+ tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
clear_global id;
Proofview.V82.of_tactic intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0b7a1e646..879145c2f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -704,7 +704,7 @@ let build_proof
in
tclTHENSEQ
[
- generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+ Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
thin dyn_infos.rec_hyps;
Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
(fun g -> observe_tac "toto" (
@@ -934,7 +934,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" *) (generalize (List.map mkVar to_revert) ))
+ ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize (List.map mkVar to_revert) )))
((* observe_tac "thin" *) (thin to_revert))
g
@@ -942,7 +942,7 @@ let id_of_decl decl = Nameops.out_name (get_name decl)
let var_of_decl decl = mkVar (id_of_decl decl)
let revert idl =
tclTHEN
- (generalize (List.map mkVar idl))
+ (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
(thin idl)
let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
@@ -1564,7 +1564,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.generalize (List.map mkVar l)) (Proofview.V82.of_tactic (clear l))
+ tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
in
let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
@@ -1610,7 +1610,7 @@ let prove_principle_for_gen
in
tclTHENSEQ
[
- generalize [lemma];
+ Proofview.V82.of_tactic (generalize [lemma]);
Proofview.V82.of_tactic (Simple.intro hid);
Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
(fun g ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index fde1b7e70..72529fbbe 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -465,7 +465,7 @@ let generalize_dependent_of x hyp g =
tclMAP
(function
| LocalAssum (id,t) when not (Id.equal id hyp) &&
- (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id])
+ (Termops.occur_var (pf_env g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
| _ -> tclIDTAC
)
(pf_hyps g)
@@ -715,7 +715,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
})
Locusops.onConcl)
;
- generalize (List.map mkVar ids);
+ Proofview.V82.of_tactic (generalize (List.map mkVar ids));
thin ids
]
else
@@ -754,7 +754,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"
- (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+ (Proofview.V82.of_tactic (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)))))
@@ -937,7 +937,7 @@ let revert_graph kn post_tac hid g =
let f_args,res = Array.chop (Array.length args - 1) args in
tclTHENSEQ
[
- generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+ Proofview.V82.of_tactic (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
@@ -981,7 +981,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
in
tclTHENSEQ[
pre_tac hid;
- generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+ Proofview.V82.of_tactic (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 c1c3801b4..10f08d3d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -689,7 +689,7 @@ let mkDestructEq :
to_revert_constr in
pf_typel new_hyps (fun _ ->
observe_tclTHENLIST (str "mkDestructEq")
- [generalize new_hyps;
+ [Proofview.V82.of_tactic (generalize new_hyps);
(fun g2 ->
let changefun patvars = { run = fun sigma ->
let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
@@ -1116,7 +1116,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.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id])))
+ tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
))
;
observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
@@ -1306,7 +1306,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 "")
[
- generalize [lemma];
+ Proofview.V82.of_tactic (generalize [lemma]);
Proofview.V82.of_tactic (Simple.intro hid);
(fun g ->
let ids = pf_ids_of_hyps g in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5c0a8226a..0fcfbfc71 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1464,7 +1464,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*
]
(Tacmach.pf_concl gl))
;
- Tactics.new_generalize env ;
+ Tactics.generalize env ;
Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)
]
end }
@@ -1726,7 +1726,7 @@ let micromega_gen
| Some (ids,ff',res') ->
(Tacticals.New.tclTHENLIST
[
- Tactics.new_generalize (List.map Term.mkVar ids) ;
+ Tactics.generalize (List.map Term.mkVar ids) ;
micromega_order_change spec res'
(Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
])
@@ -1774,7 +1774,7 @@ let micromega_order_changer cert env ff =
("__wit", cert, cert_typ)
]
(Tacmach.pf_concl gl)));
- Tactics.new_generalize env ;
+ Tactics.generalize env ;
Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)
]
end }
@@ -1812,7 +1812,7 @@ let micromega_genr prover =
(List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
(Tacticals.New.tclTHENLIST
[
- Tactics.new_generalize (List.map Term.mkVar ids) ;
+ Tactics.generalize (List.map Term.mkVar ids) ;
micromega_order_changer res' env (abstract_wrt_formula ff' ff)
])
with
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 0da630530..5f906a8da 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin"
DECLARE PLUGIN "nsatz_plugin"
TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute" constr(lt) ] -> [ Proofview.V82.tactic (Nsatz.nsatz_compute lt) ]
+| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute lt ]
END
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index fc5054080..ab33a5d2c 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1067,12 +1067,12 @@ let replay_history tactic_normalisation =
let p_initial = [P_APP 1;P_TYPE] in
let tac= shuffle_mult_right p_initial e1.body k e2.body in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ generalize_tac
[mkApp (Lazy.force coq_OMEGA17, [|
val_of eq1;
val_of eq2;
mk_integer k;
- mkVar id1; mkVar id2 |])]);
+ mkVar id1; mkVar id2 |])];
Proofview.V82.tactic (mk_then tac);
(intros_using [aux]);
Proofview.V82.tactic (resolve_id aux);
@@ -1104,7 +1104,7 @@ let replay_history tactic_normalisation =
mkVar (hyp_of_tag e1.id);
mkVar (hyp_of_tag e2.id) |])
in
- Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (generalize_tac [theorem]) (mk_then tac))) (solve_le)
+ Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le)
| DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
let id = hyp_of_tag e1.id in
let eq1 = val_of(decompile e1)
@@ -1119,7 +1119,7 @@ let replay_history tactic_normalisation =
[ Tacticals.New.tclTHENS
(Tacticals.New.tclTHENLIST [
(intros_using [aux]);
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA1,
[| eq1; rhs; mkVar aux; mkVar id |])]);
(clear [aux;id]);
@@ -1129,9 +1129,9 @@ let replay_history tactic_normalisation =
(cut (mk_gt kk izero))
[ Tacticals.New.tclTHENLIST [
(intros_using [aux1; aux2]);
- (Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_Zmult_le_approx,
- [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]));
+ [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
(clear [aux1;aux2;id]);
(intros_using [id]);
(loop l) ];
@@ -1157,7 +1157,7 @@ let replay_history tactic_normalisation =
[ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
[Tacticals.New.tclTHENLIST [
(intros_using [aux2;aux1]);
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA4,
[| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
(clear [aux1;aux2]);
@@ -1187,7 +1187,7 @@ let replay_history tactic_normalisation =
(cut state_eq)
[Tacticals.New.tclTHENLIST [
(intros_using [aux1]);
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA18,
[| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
(clear [aux1;id]);
@@ -1202,7 +1202,7 @@ let replay_history tactic_normalisation =
(cut (mk_gt kk izero))
[Tacticals.New.tclTHENLIST [
(intros_using [aux2;aux1]);
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA3,
[| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
(clear [aux1;aux2;id]);
@@ -1229,7 +1229,7 @@ let replay_history tactic_normalisation =
(cut (mk_eq eq1 (mk_inv eq2)))
[Tacticals.New.tclTHENLIST [
(intros_using [aux]);
- Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
+ (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
[| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
(clear [id1;id2;aux]);
(intros_using [id]);
@@ -1265,7 +1265,7 @@ let replay_history tactic_normalisation =
(elim_id aux);
(clear [aux]);
(intros_using [vid; aux]);
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA9,
[| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
Proofview.V82.tactic (mk_then tac);
@@ -1304,7 +1304,7 @@ let replay_history tactic_normalisation =
if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
Proofview.V82.tactic (mk_then tac);
(intros_using [id]);
@@ -1320,7 +1320,7 @@ let replay_history tactic_normalisation =
(cut (mk_gt kk2 izero))
[Tacticals.New.tclTHENLIST [
(intros_using [aux2;aux1]);
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA7, [|
eq1;eq2;kk1;kk2;
mkVar aux1;mkVar aux2;
@@ -1338,12 +1338,12 @@ let replay_history tactic_normalisation =
simpl_in_concl;
reflexivity ] ]
| CONSTANT_NOT_NUL(e,k) :: l ->
- Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
+ Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
| CONSTANT_NUL(e) :: l ->
Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
| CONSTANT_NEG(e,k) :: l ->
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]);
+ (generalize_tac [mkVar (hyp_of_tag e)]);
unfold sp_Zle;
simpl_in_concl;
unfold sp_not;
@@ -1366,7 +1366,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
let (tac,t') = normalize p_initial t in
let shift_left =
tclTHEN
- (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+ (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
(tclTRY (Proofview.V82.of_tactic (clear [id])))
in
if not (List.is_empty tac) then
@@ -1546,7 +1546,7 @@ let nat_inject =
begin try match destructurate_prop t with
Kapp(Le,[t1;t2]) ->
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
(explore [P_APP 2; P_TYPE] t2);
@@ -1555,7 +1555,7 @@ let nat_inject =
]
| Kapp(Lt,[t1;t2]) ->
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
(explore [P_APP 2; P_TYPE] t2);
@@ -1564,7 +1564,7 @@ let nat_inject =
]
| Kapp(Ge,[t1;t2]) ->
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
(explore [P_APP 2; P_TYPE] t2);
@@ -1573,7 +1573,7 @@ let nat_inject =
]
| Kapp(Gt,[t1;t2]) ->
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
(explore [P_APP 2; P_TYPE] t2);
@@ -1582,7 +1582,7 @@ let nat_inject =
]
| Kapp(Neq,[t1;t2]) ->
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
(explore [P_APP 2; P_TYPE] t2);
@@ -1592,7 +1592,7 @@ let nat_inject =
| Kapp(Eq,[typ;t1;t2]) ->
if is_conv typ (Lazy.force coq_nat) then
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 2; P_TYPE] t1);
(explore [P_APP 3; P_TYPE] t2);
@@ -1723,7 +1723,7 @@ let destructure_hyps =
then
let d1 = decidability t1 in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+ (generalize_tac [mkApp (Lazy.force coq_imp_simp,
[| t1; t2; d1; mkVar i|])]);
(onClearedName i (fun i ->
(loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit))))
@@ -1734,7 +1734,7 @@ let destructure_hyps =
begin match destructurate_prop t with
Kapp(Or,[t1;t2]) ->
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
(onClearedName i (fun i ->
(loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit))))
@@ -1742,7 +1742,7 @@ let destructure_hyps =
| Kapp(And,[t1;t2]) ->
let d1 = decidability t1 in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_not_and,
[| t1; t2; d1; mkVar i |])]);
(onClearedName i (fun i ->
@@ -1752,7 +1752,7 @@ let destructure_hyps =
let d1 = decidability t1 in
let d2 = decidability t2 in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_not_iff,
[| t1; t2; d1; d2; mkVar i |])]);
(onClearedName i (fun i ->
@@ -1764,7 +1764,7 @@ let destructure_hyps =
For t1, being decidable implies being Prop. *)
let d1 = decidability t1 in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_not_imp,
[| t1; t2; d1; mkVar i |])]);
(onClearedName i (fun i ->
@@ -1773,7 +1773,7 @@ let destructure_hyps =
| Kapp(Not,[t]) ->
let d = decidability t in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
(onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
]
@@ -1781,7 +1781,7 @@ let destructure_hyps =
(try
let thm = not_binop op in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
+ (generalize_tac
[mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
(onClearedName i (fun _ -> loop lit))
]
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 177c870b3..dca46cbcf 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1280,8 +1280,8 @@ let resolution env full_reified_goal systems_list =
CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
let decompose_tactic = decompose_tree env context solution_tree in
- Tactics.generalize
- (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
+ Proofview.V82.of_tactic (Tactics.generalize
+ (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >>
Proofview.V82.of_tactic (Tactics.change_concl reified) >>
Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
show_goal >>
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 01ebaa7b7..b1d3290aa 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -64,7 +64,7 @@ let choose_noteq eqonleft =
let mkBranches c1 c2 =
tclTHENLIST
- [Proofview.V82.tactic (generalize [c2]);
+ [generalize [c2];
Simple.elim c1;
intros;
onLastHyp Simple.case;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c3d6a65eb..d4589154f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2766,14 +2766,15 @@ let generalize_dep ?(with_let=false) c gl =
gl
(** *)
-let generalize_gen_let lconstr gl =
+let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let newcl, evd =
- List.fold_right_i (generalize_goal gl) 0 lconstr
- (Tacmach.pf_concl gl,Tacmach.project gl)
+ List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
+ (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
in
- Proofview.V82.of_tactic (Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd)
- (apply_type newcl (List.map_filter (fun ((_,c,b),_) ->
- if Option.is_empty b then Some c else None) lconstr))) gl
+ let map ((_, c, b),_) = if Option.is_empty b then Some c else None in
+ let tac = apply_type newcl (List.map_filter map lconstr) in
+ Sigma.Unsafe.of_pair (tac, evd)
+end }
let new_generalize_gen_let lconstr =
Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -2809,11 +2810,8 @@ let generalize_gen lconstr =
let new_generalize_gen lconstr =
new_generalize_gen_let (List.map (fun ((occs,c),na) ->
(occs,c,None),na) lconstr)
-
-let generalize l =
- generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
-let new_generalize l =
+let generalize l =
new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
(* Faudra-t-il une version avec plusieurs args de generalize_dep ?
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f730dd6c4..9d02d3f6d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -383,10 +383,9 @@ val letin_pat_tac : (bool * intro_pattern_naming) option ->
(** {6 Generalize tactics. } *)
-val generalize : constr list -> tactic
-val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic
+val generalize : constr list -> unit Proofview.tactic
+val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> unit Proofview.tactic
-val new_generalize : constr list -> unit Proofview.tactic
val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic
val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 14:36:55 +0000