diff --git a/src/plugins/qed/export_altergo.ml b/src/plugins/qed/export_altergo.ml
index 52864b8b16668ab498ef8c25f9eeebb6ff98629a..70087ff2d4c3fa0d889c221010c5b280ec1db11a 100644
--- a/src/plugins/qed/export_altergo.ml
+++ b/src/plugins/qed/export_altergo.ml
@@ -114,8 +114,8 @@ struct
       method op_add (_:amode) = Assoc "+"
       method op_sub (_:amode) = Assoc "-"
       method op_mul (_:amode) = Assoc "*"
-      method op_div = function Aint -> Call "comp_div" | Areal -> Op "/"
-      method op_mod = function Aint -> Call "comp_mod" | Areal -> Call "rmod"
+      method op_div = function Aint -> Call "div" | Areal -> Op "/"
+      method op_mod = function Aint -> Call "mod" | Areal -> Call "rmod"
 
       method op_eq cmode _amode =
         match cmode with
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";