diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 2b86486b245ddf26f934aac34d84d1caad3beb60..f957ff21d99f3e8d5abbc80724f86eebd5427c3e 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -479,7 +479,7 @@ val ip_of_code_annot:
 
 (** Builds the IP related to the code annotation.
     should be used only on code annotations returning a single ip, i.e.
-    assert, invariant, variant, pragma.
+    assert, invariant, variant.
     @raise Invalid_argument if the resulting code annotation has an empty set
     of identified property
     @since Carbon-20110201 *)
@@ -499,7 +499,7 @@ val ip_of_global_annotation_single:
 
 val has_status: identified_property -> bool
 (** Does the property has a logical status (which may be Never_tried)?
-    False for pragma, assumes clauses and some ACSL extensions.
+    False for assumes clauses and some ACSL extensions.
     @since 19.0-Potassium *)
 
 val get_kinstr: identified_property -> kinstr
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index e54b77b2f41f90b065bff3bf11166ff3ae83879d..11091f7b46289dc1da5ae667de797d0c4c54d2ac 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2040,11 +2040,11 @@ val visitCilBlock: cilVisitor -> block -> block
 (** Mark the given block as candidate to be flattened into its parent block,
     after returning from its visit. This is not systematic, as the environment
     might prevent it (e.g. if the preceding statement is a statement contract
-    or a slicing/pragma annotation, or if there are labels involved). Use
-    that whenever you're creating a block in order to hold multiple statements
-    as a result of visiting a single statement. If the block contains local
-    variables, it will not be marked as transient, since removing it will
-    change the scope of those variables.
+    or if there are labels involved).
+    Use that whenever you're creating a block in order to hold multiple
+    statements as a result of visiting a single statement. If the block
+    contains local variables, it will not be marked as transient, since
+    removing it will change the scope of those variables.
 
     @raise Fatal error if the given block attempts to declare local variables
     and contain definitions of local variables that are not part of the block.
diff --git a/src/plugins/sparecode/Sparecode.mli b/src/plugins/sparecode/Sparecode.mli
index 2487a7f14050471e7033329705d4c56e4d82ee99..e98a84689e1f0c7b7a91a21beed636c60e005832 100644
--- a/src/plugins/sparecode/Sparecode.mli
+++ b/src/plugins/sparecode/Sparecode.mli
@@ -27,7 +27,7 @@ module Register: sig
   val get: select_annot:bool -> select_slice_annot:bool -> Project.t
   (** Remove in each function what isn't used to compute its outputs,
       or its annotations when [select_annot] is true,
-      or its slicing pragmas when [select_slice_annot] is true.
+      or its slicing annotations when [select_slice_annot] is true.
       @return a new project where the sparecode has been removed.
   *)
 
diff --git a/src/plugins/sparecode/register.mli b/src/plugins/sparecode/register.mli
index f912136d53e7bf80cc3b0b5a4154d37e5165497f..df9ac76e7f58a22574361ab4602ef55c4a3ec99e 100644
--- a/src/plugins/sparecode/register.mli
+++ b/src/plugins/sparecode/register.mli
@@ -23,7 +23,7 @@
 val get: select_annot:bool -> select_slice_annot:bool -> Project.t
 (** Remove in each function what isn't used to compute its outputs,
     or its annotations when [select_annot] is true,
-    or its slicing pragmas when [select_slice_annot] is true.
+    or its slicing annotations when [select_slice_annot] is true.
     @return a new project where the sparecode has been removed. *)
 
 val rm_unused_globals : ?new_proj_name:string -> ?project:Project.t -> unit -> Project.t