3 files changed, 3 insertions, 2 deletions
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 1d7ee93ea3..a962547131 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -13,6 +13,6 @@ Require Export DiscrR.
 Require Export Fourier_util.
 Declare ML Module "fourier_plugin".
 
-Ltac fourier := abstract (fourierz; field; discrR).
+Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR).
 
 Ltac fourier_eq := apply Rge_antisym; fourier.
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 51bd3009ae..8e193c753e 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -462,7 +462,7 @@ let rec fourier () =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = strip_outer_cast concl in
+    let goal = Termops.strip_outer_cast 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 *)
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 7c665ae7b5..1960fa8355 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open FourierR
 
 DECLARE PLUGIN "fourier_plugin"