From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

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

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 8e193c753e..a14ec8a2ca 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -461,8 +461,9 @@ exception GoalDone
 let rec fourier () =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
+    let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = Termops.strip_outer_cast concl in
+    let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in
     let fhyp=Id.of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
-- 
cgit v1.2.3