From d5fece25d8964d5d9fcd55b66164286aeef5fb9f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Aug 2014 20:44:03 +0200 Subject: Reorganization of tactics: - made "apply" tactics of type Proofview.tactic, as well as other inner functions about elim and assert - used same hypothesis naming policy for intros and internal_cut (towards a reorganization of intro patterns) - "apply ... in H as pat" now supports any kind of introduction pattern (doc not changed) --- plugins/btauto/refl_btauto.ml | 2 +- plugins/cc/cctac.ml | 2 +- plugins/fourier/fourierR.ml | 121 +++++++++++++------------ plugins/fourier/g_fourier.ml4 | 2 +- plugins/funind/functional_principles_proofs.ml | 6 +- plugins/funind/invfun.ml | 2 +- plugins/funind/recdef.ml | 40 ++++---- plugins/omega/coq_omega.ml | 2 +- plugins/romega/refl_omega.ml | 4 +- 9 files changed, 91 insertions(+), 90 deletions(-) (limited to 'plugins') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index dbd89019e2..e6a8411534 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -248,7 +248,7 @@ module Btauto = struct let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (Tactics.change_concl changed_gl); - Proofview.V82.tactic (Tactics.apply (Lazy.force soundness)); + Tactics.apply (Lazy.force soundness); Proofview.V82.tactic (Tactics.normalise_vm_in_concl); try_unification env ] diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 70aaa0c0fc..3151a7ec75 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -486,7 +486,7 @@ let f_equal = else Tacticals.New.tclTRY (Tacticals.New.tclTHEN ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) - (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) (fun c -> Proofview.V82.tactic (apply c))))) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 7c134da7ac..a77b1d60a9 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -377,10 +377,10 @@ let tac_zero_inf_pos gl (n,d) = let tacn=ref (apply (get coq_Rlt_zero_1)) in let tacd=ref (apply (get coq_Rlt_zero_1)) in for _i = 1 to n - 1 do - tacn:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done; + tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done; for _i = 1 to d - 1 do - tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd]) + tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; + (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd]) ;; (* preuve que 0<=n*1/d @@ -391,10 +391,10 @@ let tac_zero_infeq_pos gl (n,d)= else (apply (get coq_Rle_zero_1))) in let tacd=ref (apply (get coq_Rlt_zero_1)) in for _i = 1 to n - 1 do - tacn:=(tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done; + tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done; for _i = 1 to d - 1 do - tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd]) + tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; + (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd]) ;; (* preuve que 0<(-n)*(1/d) => False @@ -402,14 +402,14 @@ let tac_zero_infeq_pos gl (n,d)= let tac_zero_inf_false gl (n,d) = if n=0 then (apply (get coq_Rnot_lt0)) else - (tclTHEN (apply (get coq_Rle_not_lt)) + (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt)) (tac_zero_infeq_pos gl (-n,d))) ;; (* preuve que 0<=(-n)*(1/d) => False *) let tac_zero_infeq_false gl (n,d) = - (tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) + (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) (tac_zero_inf_pos gl (-n,d))) ;; @@ -423,14 +423,14 @@ let my_cut c gl= let exact = exact_check;; let tac_use h = - let tac = Proofview.V82.of_tactic (exact h.hname) in + let tac = exact h.hname in match h.htype with "Rlt" -> tac |"Rle" -> tac - |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac) - |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac) - |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac) - |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac) + |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac) + |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac) + |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac) + |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac) |_->assert false ;; @@ -462,43 +462,44 @@ let mkAppL a = exception GoalDone (* Résolution d'inéquations linéaires dans R *) -let rec fourier gl= +let rec fourier () = + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = strip_outer_cast (pf_concl gl) in + let goal = strip_outer_cast concl in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) - try (let tac = - match (kind_of_term goal) with + try + match (kind_of_term goal) with App (f,args) -> (match (string_of_R_constr f) with "Rlt" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_ge_lt)) - (Proofview.V82.of_tactic (intro_using fhyp))) - fourier) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt)) + (intro_using fhyp)) + (fourier ())) |"Rle" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_gt_le)) - (Proofview.V82.of_tactic (intro_using fhyp))) - fourier) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le)) + (intro_using fhyp)) + (fourier ())) |"Rgt" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_le_gt)) - (Proofview.V82.of_tactic (intro_using fhyp))) - fourier) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt)) + (intro_using fhyp)) + (fourier ())) |"Rge" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_lt_ge)) - (Proofview.V82.of_tactic (intro_using fhyp))) - fourier) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge)) + (intro_using fhyp)) + (fourier ())) |_-> raise GoalDone) |_-> raise GoalDone - in tac gl) with GoalDone -> (* les hypothèses *) let hyps = List.map (fun (h,t)-> (mkVar h,t)) - (list_of_sign (pf_hyps gl)) in + (list_of_sign (Proofview.Goal.hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) with NoIneq -> ()) @@ -506,7 +507,7 @@ let rec fourier gl= (* lineq = les inéquations découlant des hypothèses *) if !lineq=[] then Errors.error "No inequalities"; let res=fourier_lineq (!lineq) in - let tac=ref tclIDTAC in + let tac=ref (Proofview.tclUNIT ()) in if res=[] then Errors.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) @@ -551,11 +552,11 @@ let rec fourier gl= let tc=rational_to_real cres in (* puis sa preuve *) let tac1=ref (if h1.hstrict - then (tclTHENS (apply (get coq_Rfourier_lt)) + then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt)) [tac_use h1; tac_zero_inf_pos gl (rational_to_fraction c1)]) - else (tclTHENS (apply (get coq_Rfourier_le)) + else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le)) [tac_use h1; tac_zero_inf_pos gl (rational_to_fraction c1)])) in @@ -563,20 +564,20 @@ let rec fourier gl= List.iter (fun (h,c)-> (if (!s) then (if h.hstrict - then tac1:=(tclTHENS (apply (get coq_Rfourier_lt_lt)) + then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)]) - else tac1:=(tclTHENS (apply (get coq_Rfourier_lt_le)) + else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)])) else (if h.hstrict - then tac1:=(tclTHENS (apply (get coq_Rfourier_le_lt)) + then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)]) - else tac1:=(tclTHENS (apply (get coq_Rfourier_le_le)) + else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)]))); @@ -586,43 +587,43 @@ let rec fourier gl= then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(tclTHENS (my_cut ineq) - [tclTHEN (change_concl + tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq)) + [Tacticals.New.tclTHEN (Proofview.V82.tactic (change_concl (mkAppL [| get coq_not; ineq|] - )) - (tclTHEN (apply (if sres then get coq_Rnot_lt_lt + ))) + (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt else get coq_Rnot_le_le)) - (tclTHENS (Proofview.V82.of_tactic (Equality.replace + (Tacticals.New.tclTHENS (Equality.replace (mkAppL [|get coq_Rminus;!t2;!t1|] ) - tc)) + tc) [tac2; - (tclTHENS - (Proofview.V82.of_tactic (Equality.replace + (Tacticals.New.tclTHENS + (Equality.replace (mkApp (get coq_Rinv, [|get coq_R1|])) - (get coq_R1))) + (get coq_R1)) (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) - [tclORELSE - (* TODO : Ring.polynom []*) tclIDTAC - tclIDTAC; - pf_constr_of_global (get coq_sym_eqT) (fun symeq -> - (tclTHEN (apply symeq) + [Tacticals.New.tclORELSE + (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) + (Proofview.tclUNIT ()); + Tacticals.New.pf_constr_of_global (get coq_sym_eqT) (fun symeq -> + (Tacticals.New.tclTHEN (apply symeq) (apply (get coq_Rinv_1))))] ) ])); !tac1]); - tac:=(tclTHENS (Proofview.V82.of_tactic (cut (get coq_False))) - [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None)); + tac:=(Tacticals.New.tclTHENS (cut (get coq_False)) + [Tacticals.New.tclTHEN intro (contradiction None); !tac]) |_-> assert false) |_-> assert false ); (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) - (!tac gl) + !tac (* ((tclABSTRACT None !tac) gl) *) - + end ;; (* diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 11107385da..25451fd924 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -13,5 +13,5 @@ open FourierR DECLARE PLUGIN "fourier_plugin" TACTIC EXTEND fourier - [ "fourierz" ] -> [ Proofview.V82.tactic fourier ] + [ "fourierz" ] -> [ fourier () ] END diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 1981fb837b..7f0db547d3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1433,11 +1433,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = backtrack_eqs_until_hrec hrec eqs; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) (tclTHENS (* We must have exactly ONE subgoal !*) - (apply (mkVar hrec)) + (Proofview.V82.of_tactic (apply (mkVar hrec))) [ tclTHENSEQ [ keep (tcc_hyps@eqs); - apply (Lazy.force acc_inv); + (Proofview.V82.of_tactic (apply (Lazy.force acc_inv))); (fun g -> if is_mes then @@ -1556,7 +1556,7 @@ let prove_principle_for_gen ( (* observe_tac *) (* "apply wf_thm" *) - Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])) + Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))) ) ) ) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5682c2aa47..4fcc65bda9 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -487,7 +487,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun gl -> let term = mkApp (mkVar principle_id,Array.of_list bindings) in let gl', _ty = pf_eapply Typing.e_type_of gl term in - apply term gl') + Proofview.V82.of_tactic (apply term) gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) ] diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1fa16a3015..ff35c98124 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -255,7 +255,7 @@ let tclUSER tac is_mes l g = | None -> clear [] | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l) in - tclTHENSEQ + tclTHENLIST [ clear_tac; if is_mes @@ -271,7 +271,7 @@ let tclUSER tac is_mes l g = let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = if is_mes - then tclCOMPLETE (Simple.apply (delayed_force well_founded_ltof)) + then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (delayed_force well_founded_ltof)) gl) else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress) @@ -377,12 +377,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = ) [] rev_context in let rev_ids = pf_get_new_ids (List.rev ids) g in let new_b = substl (List.map mkVar rev_ids) b in - tclTHENSEQ + tclTHENLIST [ h_intros (List.rev rev_ids); Proofview.V82.of_tactic (intro_using teq_id); onLastHypId (fun heq -> - tclTHENSEQ[ + tclTHENLIST[ thin to_intros; h_intros to_intros; (fun g' -> @@ -507,14 +507,14 @@ let rec prove_lt hyple g = let y = List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in tclTHENLIST[ - apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])); + Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (str "prove_lt") (prove_lt hyple) ] with Not_found -> ( ( tclTHENLIST[ - apply (delayed_force lt_S_n); + Proofview.V82.of_tactic (apply (delayed_force lt_S_n)); (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption)) ]) ) @@ -764,7 +764,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = ]; observe_tac (str "proving decreasing") ( tclTHENS (* proof of args < formal args *) - (apply (Lazy.force expr_info.acc_inv)) + (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv))) [ observe_tac (str "assumption") (Proofview.V82.of_tactic assumption); tclTHENLIST @@ -812,7 +812,7 @@ let rec prove_le g = in tclFIRST[ Proofview.V82.of_tactic assumption; - apply (delayed_force le_n); + Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try let matching_fun = @@ -825,7 +825,7 @@ let rec prove_le g = List.hd (List.tl args) in tclTHENLIST[ - apply(mkApp(le_trans (),[|x;y;z;mkVar h|])); + Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|]))); observe_tac (str "prove_le (rec)") (prove_le) ] with Not_found -> tclFAIL 0 (mt()) @@ -855,7 +855,7 @@ let rec make_rewrite_list expr_info max = function ) [make_rewrite_list expr_info max l; tclTHENLIST[ (* x < S max proof *) - apply (delayed_force le_lt_n_Sm); + Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm)); observe_tac (str "prove_le(2)") prove_le ] ] ) @@ -892,7 +892,7 @@ let make_rewrite expr_info l hp max = (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity))])) ; tclTHENLIST[ (* x < S (S max) proof *) - apply (delayed_force le_lt_SS); + Proofview.V82.of_tactic (apply (delayed_force le_lt_SS)); observe_tac (str "prove_le (3)") prove_le ] ]) @@ -1082,12 +1082,12 @@ let termination_proof_header is_mes input_type ids args_id relation (* this gives the accessibility argument *) observe_tac (str "apply wf_thm") - (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])) + (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))) ) ] ; (* rest of the proof *) - tclTHENSEQ + tclTHENLIST [observe_tac (str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> @@ -1206,7 +1206,7 @@ let build_and_l l = let c,tac,nb = f pl in mk_and p1 c, tclTHENS - (apply (constr_of_global conj_constr)) + (Proofview.V82.of_tactic (apply (constr_of_global conj_constr))) [tclIDTAC; tac ],nb+1 @@ -1278,7 +1278,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos build_proof Evd.empty_evar_universe_context ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in - tclTHENSEQ + tclTHENLIST [ Simple.generalize [lemma]; Proofview.V82.of_tactic (Simple.intro hid); @@ -1306,7 +1306,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos tclCOMPLETE( tclFIRST[ tclTHEN - (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) + (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))) e_assumption; Eauto.eauto_with_bases (true,5) @@ -1338,11 +1338,11 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos (tclFIRST (List.map (fun c -> - tclTHENSEQ - [Proofview.V82.of_tactic intros; + Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST + [intros; Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*); - tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto) - ] + Tacticals.New.tclCOMPLETE Auto.default_auto + ]) ) using_lemmas) ) tclIDTAC) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 271cade276..48c853029e 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -37,7 +37,7 @@ let elim_id id = Proofview.Goal.enter begin fun gl -> simplest_elim (Tacmach.New.pf_global id gl) end -let resolve_id id gl = apply (pf_global gl id) gl +let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl let timing timer_name f arg = f arg diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e22816c136..1835b6cc99 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1283,7 +1283,7 @@ let resolution env full_reified_goal systems_list = Tactics.generalize (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >> Tactics.change_concl reified >> - Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >> + Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> Tactics.normalise_vm_in_concl >> (*i Alternatives to the previous line: @@ -1292,7 +1292,7 @@ let resolution env full_reified_goal systems_list = - Skip the conversion check and rely directly on the QED: Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> i*) - Tactics.apply (Lazy.force coq_I) + Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I)) let total_reflexive_omega_tactic gl = Coqlib.check_required_library ["Coq";"romega";"ROmega"]; -- cgit v1.2.3