diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 727739689d1c62ef91ffab7e51bf0d75ed78cd04..bd263dc584ee882bb09ce53af8699955c10eb333 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8114,7 +8114,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
         (* ISO 6.7.8 para 14: final NUL added only if no size specified, or
          * if there is room for it; btw, we can't rely on zero-init of
          * globals, since this array might be a local variable *)
-        if ((not (Option.is_some leno)) ||
+        if (Option.is_none leno ||
             ((String.length s) < (integerArrayLength leno)))
         then ref [init Int64.zero]
         else ref []
@@ -8192,7 +8192,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
         (* ISO 6.7.8 para 14: final NUL added only if no size specified, or
          * if there is room for it; btw, we can't rely on zero-init of
          * globals, since this array might be a local variable *)
-        if (not (Option.is_some leno)
+        if (Option.is_none leno
             || ((List.length s) < (integerArrayLength leno)))
         then [init Int64.zero]
         else [])
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 38c943c79336126cae4616988e18ea68fd9abb85..5815b0145f26b0ab9c25bee502028062e76cdb18 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -2386,9 +2386,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
     end
   | Dvolatile(vi,rd,wr,attr,loc) ->
     let is_representative id =
-      not
-        (Option.is_some
-           (VolatileMerging.findReplacement true lvEq !currentFidx id))
+      Option.is_none
+        (VolatileMerging.findReplacement true lvEq !currentFidx id)
     in
     let push_volatile l rd wr =
       match l with
@@ -2415,8 +2414,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
            annotation can be used as is (i.e. does not overlap with a
            preceding annotation.
       *)
-      let reads = not (Option.is_some rd) || is_representative (v,R) in
-      let writes = not (Option.is_some wr) || is_representative (v,W) in
+      let reads = Option.is_none rd || is_representative (v,R) in
+      let writes = Option.is_none wr || is_representative (v,W) in
       if reads then
         if writes then
           no_drop, v::full_representative, only_reads, only_writes