diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 903e79bb9f0f115030a589126a981066f1c982b7..a0845e815040b754587d15eca7cf150ba0911b25 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -452,13 +452,13 @@ let overflowed_expr_to_term ~loc e =
   match e.enode with
   | UnOp(op, e, ty) ->
     let t = Logic_utils.expr_to_term ~coerce:true e in
-    let ty = Logic_utils.coerced ty in
-    Logic_const.term ~loc (TUnOp(op, t)) ty
+    let lty = Logic_utils.coerce_type ty in
+    Logic_const.term ~loc (TUnOp(op, t)) lty
   | BinOp(op, e1, e2, ty) ->
     let t1 = Logic_utils.expr_to_term ~coerce:true e1 in
     let t2 = Logic_utils.expr_to_term ~coerce:true e2 in
-    let ty = Logic_utils.coerced ty in
-    Logic_const.term ~loc (TBinOp(op, t1, t2)) ty
+    let lty = Logic_utils.coerce_type ty in
+    Logic_const.term ~loc (TBinOp(op, t1, t2)) lty
   | _ -> Logic_utils.expr_to_term ~coerce:true e
 
 (* Creates \is_finite((fkind)e) or \is_nan((fkind)e) according to
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index b3fa33f9651f562c46c75675870e2bdbe52f198e..183138841884800baa05c962bf843f0f48373a92 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -123,7 +123,7 @@ let plain_array_to_ptr ty =
 
 let array_to_ptr = plain_or_set plain_array_to_ptr
 
-let coerced typ =
+let coerce_type typ =
   let ty = Cil.unrollType typ in
   if Cil.isIntegralType ty then Linteger
   else if Cil.isFloatingType ty then Lreal
@@ -341,7 +341,7 @@ let is_zero_comparable t =
 
 let scalar_term_conversion conversion t =
   let loc = t.term_loc in
-  let arith_conversion t =
+  let int_conversion t =
     conversion ~loc false t (Cil.lzero ~loc ()) in
   let real_conversion ?ltyp t =
     conversion ~loc false t (Logic_const.treal_zero ~loc ?ltyp ()) in
@@ -351,14 +351,14 @@ let scalar_term_conversion conversion t =
     let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
     conversion ~loc true t (term ~loc (TDataCons(ctrue,[])) boolean_type) in
   match unroll_type t.term_type with
-  | Ctype (TInt _) -> arith_conversion t
+  | Ctype (TInt _) -> int_conversion t
   | Ctype (TFloat _) as ltyp -> real_conversion ~ltyp t
   | Ctype (TPtr _) -> ptr_conversion t
   | Ctype (TArray _) -> ptr_conversion t
   (* Could be transformed to \true: an array is never \null *)
   | Ctype (TFun _) -> ptr_conversion t
   (* decay as pointer *)
-  | Linteger -> arith_conversion t
+  | Linteger -> int_conversion t
   | Lreal -> real_conversion t
   | Ltype ({lt_name = name},[]) when name = Utf8_logic.boolean ->
     bool_conversion t
@@ -400,7 +400,7 @@ let float_builtin prefix fkind =
   | [ lf ] -> Some lf
   | _ -> Kernel.fatal "Missing or ambiguous builtin %S" name
 
-let is_float_binop op typ =
+let get_float_binop op typ =
   match typ, op with
   | TFloat(fkind,_) , PlusA  -> float_builtin "add" fkind
   | TFloat(fkind,_) , MinusA -> float_builtin "sub" fkind
@@ -408,7 +408,7 @@ let is_float_binop op typ =
   | TFloat(fkind,_) , Div    -> float_builtin "div" fkind
   | _ -> None
 
-let is_float_unop op typ =
+let get_float_unop op typ =
   match typ, op with
   | TFloat(fkind,_) , Neg  -> float_builtin "neg" fkind
   | _ -> None
@@ -419,7 +419,7 @@ let rec expr_to_term ?(coerce=false) e =
   let ctyp = Ctype typ in
   let node,ltyp =
     match e.enode with
-    | Const c -> TConst (constant_to_lconstant c) , coerced typ
+    | Const c -> TConst (constant_to_lconstant c) , coerce_type typ
     | StartOf lv -> TStartOf (lval_to_term_lval lv) , ctyp
     | AddrOf lv -> TAddrOf (lval_to_term_lval lv) , ctyp
     | BinOp (op, a, b, _) ->
@@ -427,7 +427,7 @@ let rec expr_to_term ?(coerce=false) e =
         let tc = expr_to_boolean e in
         Tif( tc , Cil.lone ~loc () , Cil.lzero ~loc () ),
         Linteger
-      else begin match is_float_binop op typ with
+      else begin match get_float_binop op typ with
         | Some phi ->
           let va = expr_to_term a in
           let vb = expr_to_term b in
@@ -435,20 +435,20 @@ let rec expr_to_term ?(coerce=false) e =
         | None ->
           let va = expr_to_term ~coerce:true a in
           let vb = expr_to_term ~coerce:true b in
-          TBinOp(op,va,vb) , coerced typ
+          TBinOp(op,va,vb) , coerce_type typ
       end
     | UnOp (LNot, c, _) ->
       let tc = expr_to_boolean c in
       Tif( tc , Cil.lzero ~loc () , Cil.lone ~loc () ),
       Linteger
     | UnOp(op, a, _) ->
-      begin match is_float_unop op typ with
+      begin match get_float_unop op typ with
         | Some phi ->
           let va = expr_to_term ~coerce:true a in
           Tapp(phi,[],[va]) , ctyp
         | None ->
           let va = expr_to_term ~coerce:true a in
-          TUnOp(op,va) , coerced typ
+          TUnOp(op,va) , coerce_type typ
       end
     | SizeOf t -> TSizeOf t, ctyp
     | SizeOfE e -> TSizeOf (Cil.typeOf e), ctyp
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 25dff3363f4146b2cf773e5c8411492e897a6a3b..6f37795a6e99c05829ac108239fe20868848a0f5 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -86,7 +86,7 @@ val logicCType : logic_type -> typ
 val array_to_ptr : logic_type -> logic_type
 
 (** C type to logic type, with implicit conversion for arithmetic types. *)
-val coerced : typ -> logic_type
+val coerce_type : typ -> logic_type
 
 (** {2 Predicates} *)
 
@@ -160,17 +160,17 @@ val pointer_comparable: ?loc:location -> term -> term -> predicate
 (** {2 Conversion from exp to term} *)
 
 val expr_to_term : ?coerce:bool -> exp -> term
-(** Returns a logic term that has exactly the same semantics than the
+(** Returns a logic term that has exactly the same semantics as the
     original C-expression. The type of the resulting term is determined
     by the [~coerce] flag as follows:
     - when [~coerce:false] is given (the default) the term has the same
-      c-type than the original expression.
+      c-type as the original expression.
     - when [~coerce:true] is given, if the original expression has an int or
       float type, then the returned term is coerced into the integer or real
       logic type, respectively.
 
     Remark: when the original expression is a comparison, it is evaluated as
-    a [_Bool] or [integer] depending on the [~coerce] flag.
+    an [int] or an [integer] depending on the [~coerce] flag.
     To obtain a boolean or predicate, use [expr_to_boolean] or
     [expr_to_predicate] instead.
 
@@ -181,7 +181,7 @@ val expr_to_predicate: exp -> predicate
 (** Returns a predicate semantically equivalent to the condition
     of the original C-expression.
 
-    This is different than [expr_to_term e |> scalar_term_to_predicate]
+    This is different from [expr_to_term e |> scalar_term_to_predicate]
     since it directly translate C-relations into logic ones.
 
     @raise Fatal error if the expression is not a comparison and cannot be
@@ -206,7 +206,7 @@ val expr_to_boolean: exp -> term
 (** Returns a boolean term semantically equivalent to the condition
     of the original C-expression.
 
-    This is different than [expr_to_term e |> scalar_term_to_predicate]
+    This is different from [expr_to_term e |> scalar_term_to_predicate]
     since it directly translate C-relations into logic ones.
 
     @raise Fatal error if the expression is not a comparison and cannot be