diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index b0203265ab29603de764b54e26f512e2a3f6826e..1e2ce76c94bed706224df1fd1a9102f898ea94e5 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -914,7 +914,7 @@ let get_stmt_annots config v s =
                 in (b_acc, (a_acc, e_acc))
           | TBRok | TBRpart ->
               let id = WpPropId.mk_assert_id config.kf s a in
-              let check = kind = Check || Wp_parameters.Assert_check_only.get ()
+              let check = kind = Check
               and goal = goal_to_select config id in
               if check && not goal then acc
               else
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index bd5be9fa57d460d53a05cfbf15a933803537d46f..3ea59dcff6c5d945d25a6a9f9ab253da7373cd73 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -897,17 +897,6 @@ module Check =
   end)
 let () = on_reset Print.clear
 
-let () = Parameter_customize.set_group wp_po
-let () = Parameter_customize.do_not_save ()
-let () = Parameter_customize.is_invisible ()
-module Assert_check_only =
-  False (struct
-    let option_name = "-wp-assert-check-only"
-    let help =
-      "Turns assertions into labels."
-  end)
-let () = on_reset Print.clear
-
 (* -------------------------------------------------------------------------- *)
 (* --- OS environment variables                                           --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 724fc39ae5178e2b2c0bd50017e97b01e84adf47..88dfd0553b3f8aea5e6db86da44a6c4a8de29157 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -135,7 +135,6 @@ module ReportJson: Parameter_sig.String
 module ReportName: Parameter_sig.String
 module MemoryContext: Parameter_sig.Bool
 module Check: Parameter_sig.Bool
-module Assert_check_only: Parameter_sig.Bool
 
 (** {2 Environment Variables} *)