From cd186218344cdec50b4333ecbad61eec48911f3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Apr 2019 10:27:25 +0200
Subject: [PATCH] [wp/coq] fix coq dependencies

---
 src/plugins/wp/share/wp.driver                       | 12 ++++++------
 .../wp/tests/wp_plugin/oracle/inductive.res.oracle   |  6 ++++++
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 44a2fedb5ae..17c5507e275 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 d012a5d99d0..72d899e2d0d 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.
   
-- 
GitLab