[wp/coq] fix coq dependencies

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";

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.