diff --git a/src/plugins/wp/share/ergo/Cbits.mlw b/src/plugins/wp/share/ergo/Cbits.mlw
index 1bf6749cffed1c9e2e168e513d1960e72b6f64e5..4b2b2d6ed430f12ce4b1c5e3ee9a1380be4a3f7e 100644
--- a/src/plugins/wp/share/ergo/Cbits.mlw
+++ b/src/plugins/wp/share/ergo/Cbits.mlw
@@ -27,14 +27,12 @@
 (** The theory bool_Bool_ must be appended to this file*)
 (** The theory int_Int_ must be appended to this file*)
 (** The theory int_Abs_ must be appended to this file*)
-(** The theory int_EuclideanDivision_ must be appended to this file*)
 (** The theory int_ComputerDivision_ must be appended to this file*)
 (** The theory real_Real_ must be appended to this file*)
 (** The theory real_RealInfix_ must be appended to this file*)
 (** The theory real_FromInt_ must be appended to this file*)
-(** The theory for_drivers_ComputerOfEuclideanDivision_ must be appended to this file*)
 (** The theory Cint_ must be appended to this file*)
-<<<<<<< HEAD
+
 logic bit_testb : int, int -> bool
 
 logic bit_test : int, int -> prop
@@ -51,8 +49,6 @@ logic lsl : int, int -> int
 
 logic lsr : int, int -> int
 
-||||||| merged common ancestors
-=======
 axiom lnot_bool : (lnot(0) = (-1))
 
 axiom lnot_bool1 : (lnot((-1)) = 0)
@@ -87,7 +83,6 @@ axiom lxor_0 : (forall x:int [lxor(0, x)]. (lxor(0, x) = x))
 
 axiom lxor_0bis : (forall x:int [lxor(x, 0)]. (lxor(x, 0) = x))
 
->>>>>>> origin/master
 axiom bit_test_def :
   (forall x:int. forall k:int [bit_testb(x, k)]. ((bit_testb(x, k) = true) ->
   bit_test(x, k)))
@@ -536,4 +531,3 @@ axiom lor_addition :
 axiom lxor_addition :
   (forall x:int. forall y:int [land(x, y), lxor(x, y)]. ((land(x, y) = 0) ->
   ((x + y) = lxor(x, y))))
-
diff --git a/src/plugins/wp/share/ergo/Qed.mlw b/src/plugins/wp/share/ergo/Qed.mlw
index 0537e4c35cbdb14341fcfade5481df37a862b5b0..eeb3d92f8822c9f0c0e116425e7e9c457119cfca 100644
--- a/src/plugins/wp/share/ergo/Qed.mlw
+++ b/src/plugins/wp/share/ergo/Qed.mlw
@@ -26,12 +26,10 @@
 (** The theory bool_Bool_ must be appended to this file*)
 (** The theory int_Int_ must be appended to this file*)
 (** The theory int_Abs_ must be appended to this file*)
-(** The theory int_EuclideanDivision_ must be appended to this file*)
 (** The theory int_ComputerDivision_ must be appended to this file*)
 (** The theory real_Real_ must be appended to this file*)
 (** The theory real_RealInfix_ must be appended to this file*)
 (** The theory real_FromInt_ must be appended to this file*)
-(** The theory for_drivers_ComputerOfEuclideanDivision_ must be appended to this file*)
 logic match_bool : bool, 'a, 'a -> 'a
 
 axiom match_bool1 :
diff --git a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw b/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
index ab250caabbfa9ce388e6699ec584ccd4e0fd172b..4fca9c6c375416d431f1e8a4491f37f58da2b61f 100644
--- a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
+++ b/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
@@ -17,8 +17,8 @@
 (** The theory Bool_ must be appended to this file*)
 (** The theory int_Int_ must be appended to this file*)
 (** The theory int_Abs_ must be appended to this file*)
-(** The theory int_EuclideanDivision_ must be appended to this file*)
 (** The theory int_ComputerDivision_ must be appended to this file*)
+
 axiom cdiv_cases :
   (forall n:int. forall d:int [div(n, d)]. ((0 <= n) -> ((0 <  d) -> (div(n,
   d) = (n / d)))))
@@ -50,4 +50,3 @@ axiom cmod_cases2 :
 axiom cmod_cases3 :
   (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((d <  0) -> (mod(n,
   d) = (-((-n) % (-d)))))))
-
diff --git a/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw b/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw
deleted file mode 100644
index 7390354ffaa31e89b8924bf338a7840b799894f5..0000000000000000000000000000000000000000
--- a/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw
+++ /dev/null
@@ -1,5 +0,0 @@
-(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
-(** The theory int_Int_ must be appended to this file*)
-(** The theory int_Abs_ must be appended to this file*)
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 271c470da94179003bfc30a861aa583070eb56e7..84cccb44f4c62d6bec8d985a038acc447e61238e 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -41,7 +41,6 @@ why3.import += "frama_c_wp.qed.Qed";
 altergo.file += "ergo/int.Int.mlw";
 altergo.file += "ergo/int.Abs.mlw";
 altergo.file += "ergo/int.ComputerDivision.mlw";
-altergo.file += "ergo/int.EuclideanDivision.mlw";
 altergo.file += "ergo/int.ComputerOfEuclideanDivision.mlw";
 altergo.file += "ergo/real.Real.mlw";
 altergo.file += "ergo/real.RealInfix.mlw";