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 +++---
 plugins/firstorder/rules.ml | 9 +++++----
 plugins/fourier/fourierR.ml | 4 ++--
 3 files changed, 10 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2d9dec095a..b2c609dcbc 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 a60fd4d8f1..96601f74a2 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 e11cbc279a..25d8f8c832 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)))]
 
 					 )
 				]));
-- 
cgit v1.2.3