From b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:41:55 +0200 Subject: Put the "generalize" tactic in the monad. --- plugins/decl_mode/decl_proof_instr.ml | 6 +-- plugins/firstorder/instances.ml | 8 ++-- plugins/firstorder/rules.ml | 8 ++-- plugins/funind/functional_principles_proofs.ml | 10 ++--- plugins/funind/invfun.ml | 10 ++--- plugins/funind/recdef.ml | 6 +-- plugins/micromega/coq_micromega.ml | 8 ++-- plugins/nsatz/g_nsatz.ml4 | 2 +- plugins/omega/coq_omega.ml | 58 +++++++++++++------------- plugins/romega/refl_omega.ml | 4 +- 10 files changed, 60 insertions(+), 60 deletions(-) (limited to 'plugins') 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 >> -- cgit v1.2.3