Removes references to removed pragma in some comments.

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

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.

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.
   *)
 

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