From d272cd02ef9ba2509c266f58ee39f51106ae53c2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Apr 2017 14:27:24 +0200 Subject: 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. --- plugins/cc/cctac.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/cc') 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 -> -- cgit v1.2.3