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/fourier/fourierR.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/fourier')

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