diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 94ff33306fc61bb8fb649f3a2d00eee25097fe91..eb88284cee5c2e28b1f0e347c0cbfc3208430d4d 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -751,7 +751,7 @@ let compute_r_common r1 m1 r2 m2 =
      solutions (k1,k2) to (E2).
 
      Let d = pgcd(m1,m2). There are solutions to (E2) only if d
-     divides c (because d divides k1*m1 - k2*m2). Else we raise
+     divides r (because d divides k1*m1 - k2*m2). Else we raise
      [Error_Bottom]. *)
   let (x1,_,pgcd) = extended_euclidian_algorithm m1 m2 in
   let r = Int.sub r2 r1 in
@@ -762,7 +762,7 @@ let compute_r_common r1 m1 r2 m2 =
   (* The extended euclidian algorithm has provided solutions x1,x2 to
      the Bezout identity x1*m1 + x2*m2 = d.
 
-     x1*m1 + x2*m2 = d ==> x1*(c/d)*m1 + x2*(r/d)*m2 = d*(r/d).
+     x1*m1 + x2*m2 = d ==> x1*(r/d)*m1 + x2*(r/d)*m2 = d*(r/d).
 
      Thus, k1 = x1*(r/d), k2=-x2*(r/d) are solutions to (E2)
      Thus, x = r1 + x1*(r/d)*m1 is a particular solution to (E1). *)
@@ -1681,7 +1681,7 @@ let div x y =
    elements [x mod f] for [x] in [v].
 
    [scale_rem ~pos:true f v] is an over-approximation of the set of
-   elements [x pos_rem f] for [x] in [v].
+   elements [x e_rem f] for [x] in [v].
 *)
 let scale_rem ~pos f v =
 (*     Format.printf "scale_rem %b %a %a@."
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index b4f3e5a485b8c26e3936e919e65ade6a44346eef..32218fd774658eb5f127b9d0603a205fd1b8153e 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -237,25 +237,25 @@ val scale : Integer.t -> t -> t
 
 val scale_div : pos:bool -> Integer.t -> t -> t
 (** [scale_div ~pos:false f v] is an over-approximation of the set of
-    elements [x / f] for [x] in [v].
+    elements [x c_div f] for [x] in [v].
 
     [scale_div ~pos:true f v] is an over-approximation of the set of
-    elements [x pos_div f] for [x] in [v]. *)
+    elements [x e_div f] for [x] in [v]. *)
 
 val scale_div_under : pos:bool -> Integer.t -> t -> t
 (** [scale_div_under ~pos:false f v] is an under-approximation of the
-    set of elements [x / f] for [x] in [v].
+    set of elements [x c_div f] for [x] in [v].
 
     [scale_div_under ~pos:true f v] is an under-approximation of the
-    set of elements [x pos_div f] for [x] in [v]. *)
+    set of elements [x e_div f] for [x] in [v]. *)
 
 val div : t -> t -> t (** Integer division *)
 val scale_rem : pos:bool -> Integer.t -> t -> t
 (** [scale_rem ~pos:false f v] is an over-approximation of the set of
-    elements [x mod f] for [x] in [v].
+    elements [x c_rem f] for [x] in [v].
 
     [scale_rem ~pos:true f v] is an over-approximation of the set of
-    elements [x pos_rem f] for [x] in [v]. *)
+    elements [x e_rem f] for [x] in [v]. *)
 
 val c_rem : t -> t -> t
 val mul : t -> t -> t
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 8f6fffda5468e24515d8bc96e5214c8ccb4e2a04..58c641c2c8083165291b3cfd3a446bdee9c77d01 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -61,7 +61,7 @@ val e_div : t -> t -> t
     Equivalent to C division if both operands are positive.
     Equivalent to a floored division if b > 0 (rounds downwards),
     otherwise rounds upwards.
-    Note: it is possible that pos_div (-a) b <> pos_div a (-b).
+    Note: it is possible that e_div (-a) b <> e_div a (-b).
 *)
 
 val e_rem : t -> t -> t
@@ -81,7 +81,7 @@ val c_rem : t -> t -> t
     Implemented by [Z.rem] *)
 
 val c_div_rem : t -> t -> t * t
-(** Remainder of the truncated division towards 0 (like in C99.
+(** [c_div_rem a b] returns [(c_div a b, c_rem a b)].
     Implemented by [Z.div_rem] *)
 
 val pgcd : t -> t -> t