diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index c39540eb78cb8656a788c56fd49768de353a2fa7..df6e83336874b7a7fd735a30a60fbf3bb0c214ff 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -69,7 +69,7 @@ val precondition : goal:bool -> funspec -> predicate
     With [~goal:true], only returns assert and check predicates.
     With [~goal:false], only returns assert and admit predicates.
     @since Carbon-20101201
-    @modify 23.0-Vanadium introduce [goal] flag
+    @before 23.0-Vanadium no [goal] flag.
 *)
 
 val behavior_assumes : funbehavior -> predicate
@@ -80,14 +80,14 @@ val behavior_precondition : goal:bool -> funbehavior -> predicate
 (** Builds the precondition from [b_assumes] and [b_requires] clauses.
     For flag [~goal] see {!Ast_info.precondition} above.
     @since Carbon-20101201
-    @modify 23.0-Vanadium introduce [goal] flag
+    @before 23.0-Vanadium no [goal] flag.
 *)
 
 val behavior_postcondition :
   goal:bool -> funbehavior -> termination_kind -> predicate
 (** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
     For flag [~goal] see {Ast_info.precondition} above.
-    @modify 23.0-Vanadium introduce [goal] flag
+    @before 23.0-Vanadium no [goal] flag.
 *)
 
 val disjoint_behaviors : funspec -> string list -> predicate
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index 0b2328bbdadc735228139b4a4a20a10bd4649539..572ee38ca0221df19644f0e79d27e961e1b6d87e 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -311,7 +311,7 @@ val add_aliases:
     If [deprecated] is set to true, the use of the aliases emits a warning.
     @Invalid_argument if an alias name is the empty string
     @since Carbon-20110201
-    @modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
+    @before 22.0-Titanium no [visible] and [deprecated] arguments. *)
 
 val replace_option_setting:
   string -> plugin:string -> group:Group.t -> option_setting -> unit
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 53b574e69211c61489bfc26f6e44ebf92c2ad024..b5558a5aa42f0b5a808ff2402cb2480d6afc9354 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -190,7 +190,7 @@ module type S_no_parameter = sig
       If [visible] is set to false, the aliases do not appear in help messages.
       If [deprecated] is set to true, the use of the aliases emits a warning.
       @raise Invalid_argument if one of the strings is empty
-      @modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
+      @before 22.0-Titanium no [visible] and [deprecated] arguments. *)
 
   (**/**)
   val is_set: unit -> bool