diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index 4ed6b2e99cf0f1730ac0f7e5266ab9d5b4cdd530..5ada1ac419b1ae0fedb9b8ea4cb13f4d9d384554 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -192,7 +192,7 @@ module PreCondAt =
 let rec transpose_precondition stmt pid kf funcexp args =
   let formals = Kernel_function.get_formals kf in
   let ip = match pid with
-    | Property.(IPPredicate {ip_pred}) -> ip_pred
+    | Property.IPPredicate {Property.ip_pred} -> ip_pred
     | _ -> assert false
   in
   let ip = transpose_pred_at_callsite ~formals ~concretes:args ip in
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index ebf393201e4a855b32cd68b1459036c3a6f09f83..42d4efc5b6b7b0c5dd496079cae80938da45c3f6 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -221,13 +221,13 @@ struct
       | Instr (Call _)
       | Instr (Local_init (_, ConsInit _, _)) ->
         let extract_instance_predicate = function
-          | Property.(IPPropertyInstance {ii_pred}) -> ii_pred
+          | Property.IPPropertyInstance {Property.ii_pred} -> ii_pred
           (* Other cases should not happen, unless a plugin has replaced call
              preconditions. In this case, print nothing but do not crash. *)
           | _ -> raise Not_found
         in
         let extract_predicate = function
-          | Property.(IPPredicate {ip_pred}) -> ip_pred
+          | Property.IPPredicate {Property.ip_pred} -> ip_pred
           | _ -> assert false
         in
         (* Functons called at this point *)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index fe381109caf4ca4d4dfd3cde4a3c71d677a062db..8be6e60977eb4b749d26e68d8d22d41d1eb1149a 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -775,7 +775,7 @@ let highlighter (buffer:reactive_buffer) localizable ~start ~stop =
        'Unknown'. *)
     let filter (ip_src, _ip_copy) =
       match ip_src with
-      | Property.(IPPredicate {ip_kind=PKRequires bhv}) ->
+      | Property.IPPredicate {Property.ip_kind=PKRequires bhv} ->
         bhv.b_assumes = []
       | _ -> false
     in
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index b7d6a7ad039857b91d06f2a260b104ed7ad2e3d0..4ec633c711ce24d107fbb2ec27359d5bf788f63a 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -188,7 +188,7 @@ let get_results () =
       aux_statuses (fun st -> Property.Hashtbl.add statuses ip st) ip
     in
     match ip with
-    | Property.(IPCodeAnnot {ica_ca}) -> begin
+    | Property.IPCodeAnnot {Property.ica_ca} -> begin
         match Alarms.find ica_ca with
         | None -> (* real property *) add ()
         | Some _ -> (* alarm; do not save it here *) ()
@@ -496,7 +496,7 @@ let make_report ()  =
   let report = empty_report () in
   let report_property ip =
     match ip with
-    | Property.(IPCodeAnnot {ica_ca}) ->
+    | Property.IPCodeAnnot {Property.ica_ca} ->
       begin
         let status = get_status ip in
         match Alarms.find ica_ca with
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 6164537a9de9a562cffeec713b5df437350f1096..2a72d9e6b032833fb7532cd4c9a371db7496f2cd 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -305,8 +305,9 @@ let filter_assign config pid =
 
 let filter_speconly config pid =
   if Cil2cfg.cfg_spec_only config.cfg then
+    let open Property in
     match WpPropId.property_of_id pid with
-    | Property.(IPPredicate {ip_kind = PKRequires _; ip_kinstr = Kglobal}) -> true
+    | IPPredicate {ip_kind = PKRequires _; ip_kinstr = Kglobal} -> true
     | _ -> false
   else true
 
@@ -1336,8 +1337,9 @@ let get_strategies assigns kf model behaviors ki property =
 let get_precond_strategies ~model p =
   debug "[get_precond_strategies] %s@."
     (Property.Names.get_prop_name_id p);
+  let open Property in
   match p with
-  | Property.(IPPredicate {ip_kind = PKRequires b; ip_kf; ip_kinstr = Kglobal}) ->
+  | IPPredicate {ip_kind = PKRequires b; ip_kf; ip_kinstr = Kglobal} ->
       let strategies =
         if WpStrategy.is_main_init ip_kf then
           get_strategies NoAssigns ip_kf model [b.b_name] None (IdProp p)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index f05d72b2ece269d946a29a3da8a12bf4ef86b434..ee456686522018f540bd0c8641fa71e1720e1d63 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -577,11 +577,12 @@ let kinstr_hints hs = function
   | Kglobal -> ()
 
 let propid_hints hs p =
+  let open Property in
   match p.p_kind , p.p_prop with
   | PKCheck , _ -> ()
-  | PKProp , Property.(IPAssigns {ias_kinstr=Kstmt _}) ->
+  | PKProp , IPAssigns {ias_kinstr=Kstmt _} ->
       add_required hs "stmt-assigns"
-  | PKProp , Property.(IPAssigns {ias_kinstr=Kglobal}) ->
+  | PKProp , IPAssigns {ias_kinstr=Kglobal} ->
       add_required hs "fct-assigns"
   | PKPropLoop , Property.IPAssigns _ -> add_required hs "loop-assigns"
   | PKPropLoop , _ -> add_required hs "invariant"
@@ -709,9 +710,10 @@ let is_assigns p =
   | Property.IPAssigns _ -> true
   | _ -> false
 
-let is_requires = function
-  | Property.(IPPredicate {ip_kind = PKRequires _}) -> true
-  | _ -> false
+let is_requires =
+  let open Property in function
+    | IPPredicate {ip_kind = PKRequires _} -> true
+    | _ -> false
 
 let is_loop_preservation p =
   match p.p_kind with