diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-11 14:27:24 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-24 17:59:21 +0200 |
commit | d272cd02ef9ba2509c266f58ee39f51106ae53c2 (patch) | |
tree | 506223959f09e7c9f8f2b4d6ac6c4261daf9480a | |
parent | 1ef92c718ece547826f4c7e5c1ce78a6965e1ca6 (diff) |
Fix the API of the new pf_constr_of_global.
The current implementation was still using continuation passing-style, and
furthermore was triggering a focus on the goals. We take advantage of the
tactic features instead.
-rw-r--r-- | plugins/cc/cctac.ml | 6 | ||||
-rw-r--r-- | plugins/firstorder/rules.ml | 9 | ||||
-rw-r--r-- | plugins/fourier/fourierR.ml | 4 | ||||
-rw-r--r-- | tactics/equality.ml | 6 | ||||
-rw-r--r-- | tactics/tacticals.ml | 14 | ||||
-rw-r--r-- | tactics/tacticals.mli | 2 | ||||
-rw-r--r-- | tactics/tactics.ml | 6 |
7 files changed, 23 insertions, 24 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2d9dec095..b2c609dcb 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -245,7 +245,7 @@ let app_global f args k = Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) let new_app_global f args k = - Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args)) let new_refine c = Proofview.V82.tactic (refine c) let refine c = refine c @@ -492,7 +492,7 @@ let congruence_tac depth l = *) let mk_eq f c1 c2 k = - Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in @@ -501,7 +501,7 @@ let mk_eq f c1 c2 k = let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) - end }) + end } let f_equal = Proofview.Goal.enter { enter = begin fun gl -> diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index a60fd4d8f..96601f74a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -14,6 +14,7 @@ open Vars open Tacmach open Tactics open Tacticals +open Proofview.Notations open Termops open Formula open Sequent @@ -96,7 +97,7 @@ let left_and_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE (tclTHENLIST - [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim); + [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim); clear_global id; tclDO n (Proofview.V82.of_tactic intro)]) (wrap n false continue seq) @@ -110,12 +111,12 @@ let left_or_tac ind backtrack id continue seq gls= tclDO n (Proofview.V82.of_tactic intro); wrap n false continue seq] in tclIFTHENSVELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim)) (Array.map f v) backtrack gls let left_false_tac id= - Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) + Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim) (* left arrow connective rules *) @@ -183,7 +184,7 @@ let forall_tac backtrack continue seq= let left_exists_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim)) (tclTHENLIST [clear_global id; tclDO n (Proofview.V82.of_tactic intro); (wrap (n-1) false continue seq)]) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index e11cbc279..25d8f8c83 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -617,9 +617,9 @@ let rec fourier () = [Tacticals.New.tclORELSE (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq -> + Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq -> (Tacticals.New.tclTHEN (apply symeq) - (apply (get coq_Rinv_1))))] + (apply (get coq_Rinv_1)))] ) ])); diff --git a/tactics/equality.ml b/tactics/equality.ml index e68be91e9..25c28cf4a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -658,8 +658,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in - Tacticals.New.pf_constr_of_global sym (fun sym -> - Tacticals.New.pf_constr_of_global e (fun e -> + Tacticals.New.pf_constr_of_global sym >>= fun sym -> + Tacticals.New.pf_constr_of_global e >>= fun e -> let eq = applist (e, [t1;c1;c2]) in tclTHENLAST (replace_core clause l2r eq) @@ -667,7 +667,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = [assumption; tclTHEN (apply sym) assumption; try_prove_eq - ]))) + ]) end } let replace c1 c2 = diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5c97f27ba..c8441a8cc 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -732,13 +732,11 @@ module New = struct let case_nodep_then_using = general_elim_then_using gl_make_case_nodep false - let pf_constr_of_global ref tac = - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (sigma, c) = Evd.fresh_global env sigma ref in - let c = EConstr.of_constr c in - Proofview.Unsafe.tclEVARS sigma <*> (tac c) - end } + let pf_constr_of_global ref = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.tclENV >>= fun env -> + let (sigma, c) = Evd.fresh_global env sigma ref in + let c = EConstr.of_constr c in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 01b9e5e93..5a4ecbac7 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -263,5 +263,5 @@ module New : sig val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic + val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1615aec89..9c2a1d850 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4721,7 +4721,7 @@ let symmetry_red allowred = | Some eq_data,_,_ -> Tacticals.New.tclTHEN (convert_concl_no_check concl DEFAULTcast) - (Tacticals.New.pf_constr_of_global eq_data.sym apply) + (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind end } @@ -4817,8 +4817,8 @@ let transitivity_red allowred t = Tacticals.New.tclTHEN (convert_concl_no_check concl DEFAULTcast) (match t with - | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply - | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t])) + | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply + | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t]) | None,eq,eq_kind -> match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") |