diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 2810d1add1cc3d27a7526b21ad4c54d8e010d659..11aeaa41e39e9378a306c1a3a400babb3e64640f 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -305,7 +305,7 @@ let build_automaton ~annotations kf =
   in
   let build_stmt_transition src dest stmt succ transition =
     ignore (build_stmt_next src dest stmt succ transition) in
-  
+
   let rec do_list do_one control labels = function
     | [] -> assert false
     | stmt :: [] -> do_one control labels stmt
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index 5827e2b3b2476c2ee86493dadfe833a518b4f2fa..19c83200459f21b4665f2e8d202f5527cb776163 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -65,7 +65,7 @@ let apply task ~kf ?bhvs ?prop () =
     List.iter (fun bhv ->
         task.modes <- { kf ; bhv } :: task.modes
       ) bhvs ;
-    Extlib.may (fun ip -> task.props <- `PropId ip) prop ;
+    Option.iter (fun ip -> task.props <- `PropId ip) prop ;
   end
 
 let notyet prop =