From 01849481fbabc3a3fa6c483e703996b01e37fca5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 01:25:11 +0100
Subject: Removing compatibility layers from Tacticals

---
 plugins/fourier/fourierR.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index bffca62231..ec73fccb5b 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -616,7 +616,7 @@ let rec fourier () =
                                    (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
                                    (Proofview.tclUNIT ());
 				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq ->
-					  (Tacticals.New.tclTHEN (apply (EConstr.of_constr symeq))
+					  (Tacticals.New.tclTHEN (apply symeq)
 						(apply (get coq_Rinv_1))))]
 
 					 )
-- 
cgit v1.2.3