diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 44a2fedb5aec91248190e647fb2fae27c136de46..17c5507e2754228c45c1a0f1c245824786850002 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -30,6 +30,7 @@ coq.file += "coqwp:real/Real.v";
 coq.file += "coqwp:real/RealInfix.v";
 coq.file += "coqwp:real/FromInt.v";
 coq.file += "coqwp:map/Map.v";
+coq.file += "coqwp:bool/Bool.v";
 coq.file += "coqwp/Qedlib.v";
 coq.file += "coqwp/Qed.v";
 why3.import += "int.Abs:IAbs";
@@ -48,7 +49,6 @@ why3.import += "map.Const";
 altergo.file += "ergo/map.Const.mlw";
 
 library bool:
-coq.file += "coqwp:bool/Bool.v";
 altergo.file += "ergo/bool.Bool.mlw";
 
 library minmax_int:
@@ -74,21 +74,20 @@ logic real "\\min"(real,real) =
       {coq="Rmin";altergo="min_real";why3="Rg.min"};
 
 library cint:
+coq.file += "coqwp/Bits.v";
+coq.file += "coqwp/Zbits.v";
 coq.file += "coqwp/Cint.v";
 why3.file += "why3/Cint.why";
 altergo.file += "ergo/Cint.mlw";
 
 library cbits: cint
-coq.file += "coqwp/Bits.v";
-coq.file += "coqwp/Zbits.v";
 coq.file += "coqwp/Cbits.v";
 altergo.file += "ergo/Cbits.mlw";
 why3.file += "why3/Cbits.why";
 
-library cfloat: cmath
+library cfloat: cmath sqrt
 coq.file += "coqwp/Cfloat.v";
 why3.file += "why3/Cfloat.why";
-altergo.file += "ergo/real.Square.mlw";
 altergo.file += "ergo/Cfloat.mlw";
 type "rounding_mode"   = "rounding_mode";
 ctor "\\Up"()            = "Up";
@@ -127,7 +126,6 @@ altergo.file := "ergo/Memory.mlw";
 
 library sqrt: cmath
 why3.import += "real.Square";
-coq.file += "coqwp:real/Square.v";
 coq.file += "coqwp/Square.v";
 why3.file += "why3/Square.why";
 altergo.file += "ergo/real.Square.mlw";
@@ -153,6 +151,8 @@ altergo.file += "ergo/real.Truncate.mlw" ;
 library cmath: qed
 why3.import += "real.Abs:RAbs" ;
 why3.file += "why3/Cmath.why";
+coq.file += "coqwp:real/Abs.v" ;
+coq.file += "coqwp:real/Square.v";
 coq.file += "coqwp/Cmath.v";
 altergo.file += "ergo/real.Abs.mlw" ;
 altergo.file += "ergo/Cmath.mlw";
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index d012a5d99d0d9cfc14cc1d5c3ade96154f062306..72d899e2d0d74018180d7d565cc49af2c19c4761 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -12,6 +12,7 @@
   Require Import ZArith.
   Require Import Reals.
   Require Import BuiltIn.
+  Require Import HighOrd.
   Require Import int.Int.
   Require Import int.Abs.
   Require Import int.ComputerDivision.
@@ -19,6 +20,7 @@
   Require Import real.RealInfix.
   Require Import real.FromInt.
   Require Import map.Map.
+  Require Import bool.Bool.
   Require Import Qedlib.
   Require Import Qed.
   Require Import Memory.
@@ -34,6 +36,7 @@
   Require Import ZArith.
   Require Import Reals.
   Require Import BuiltIn.
+  Require Import HighOrd.
   Require Import int.Int.
   Require Import int.Abs.
   Require Import int.ComputerDivision.
@@ -41,6 +44,7 @@
   Require Import real.RealInfix.
   Require Import real.FromInt.
   Require Import map.Map.
+  Require Import bool.Bool.
   Require Import Qedlib.
   Require Import Qed.
   
@@ -80,6 +84,7 @@
   Require Import ZArith.
   Require Import Reals.
   Require Import BuiltIn.
+  Require Import HighOrd.
   Require Import int.Int.
   Require Import int.Abs.
   Require Import int.ComputerDivision.
@@ -87,6 +92,7 @@
   Require Import real.RealInfix.
   Require Import real.FromInt.
   Require Import map.Map.
+  Require Import bool.Bool.
   Require Import Qedlib.
   Require Import Qed.