From c2a3851f663be37360e9e90438bbf7be9f4162ea Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 20 Apr 2022 14:58:47 +0200
Subject: [PATCH] [Kernel] more @modify -> @before tags

---
 src/kernel_services/ast_queries/ast_info.mli             | 6 +++---
 src/kernel_services/cmdline_parameters/cmdline.mli       | 2 +-
 src/kernel_services/cmdline_parameters/parameter_sig.mli | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index c39540eb78c..df6e8333687 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 0b2328bbdad..572ee38ca02 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 53b574e6921..b5558a5aa42 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
-- 
GitLab