diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index a45458db4a8e2e45fad08bb5e3f95c4aa16a51fd..2fb2f16fed142915eca73e2608c793101ca59cf3 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -96,12 +96,12 @@ coq.file += "coqwp:real/Abs.v";
 coq.file += "coqwp/Cfloat.v";
 why3.import += "frama_c_wp.cfloat.Cfloat";
 altergo.file += "ergo/Cfloat.mlw";
-type "rounding_mode"   = "rounding_mode";
-ctor "\\Up"()            = "Up";
-ctor "\\Down"()          = "Down";
-ctor "\\ToZero"()        = "ToZero";
-ctor "\\NearestAway"()   = "NearestTiesToAway";
-ctor "\\NearestEven"()   = "NearestTiesToEven";
+type "rounding_mode"   = "Rounding.mode";
+ctor "\\Up"()          = "Rounding.RTP";
+ctor "\\Down"()        = "Rounding.RTN";
+ctor "\\ToZero"()      = "Rounding.RTZ";
+ctor "\\NearestAway"() = "Rounding.RNA";
+ctor "\\NearestEven"() = "Rounding.RNE";
 predicate "\\is_finite"(float32) = "is_finite_f32";
 predicate "\\is_finite"(float64) = "is_finite_f64";
 predicate "\\is_NaN"(float32) = "is_NaN_f32";
@@ -112,8 +112,8 @@ predicate "\\is_plus_infinity"(float32) = "is_positive_infinite_f32";
 predicate "\\is_plus_infinity"(float64) = "is_positive_infinite_f64";
 predicate "\\is_minus_infinity"(float32) = "is_negative_infinite_f32";
 predicate "\\is_minus_infinity"(float64) = "is_negative_infinite_f64";
-logic bool "\\round_float"(rounding_mode,real) = "round_float";
-logic bool "\\round_double"(rounding_mode,real) = "round_double";
+logic float32 "\\round_float"(rounding_mode,real) = "round_float";
+logic float64 "\\round_double"(rounding_mode,real) = "round_double";
 
 library vset:
 type set = "set";