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 /tactics | |
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.
Diffstat (limited to 'tactics')
-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 |
4 files changed, 13 insertions, 15 deletions
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.") |