diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index fa0f3c01ef3fac3fa84bd85314a148cf542217da..2411abb40fa31470341b7d1219e21d06f43dbd80 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -2809,7 +2809,7 @@ a new one is loaded\index{Loading} from disk).
\scodeidxdef{File}{init\_project\_from\_visitor};
or write the following line of code (see Section~\ref{proj:selection}):
\scodeidx{Project}{clear}
- \sscodeidx{State\_selection}{S}{only\_dependencies}
+ \scodeidx{State\_selection}{only\_dependencies}
\scodeidx{Ast}{self}
\begin{alltt}
let selection = State_selection.only_dependencies Ast.self in
@@ -2918,7 +2918,7 @@ consistently handle state dependencies\index{State!Dependency}.
The following statement clears all the results of the value analysis and all
its dependencies in the current project.\index{State!Cleaning}
\scodeidx{Project}{clear}
- \sscodeidx{State\_selection}{S}{with\_dependencies}
+ \scodeidx{State\_selection}{with\_dependencies}
\sscodeidx{Db}{Value}{self}
\begin{ocamlcode}
let selection = State_selection.with_dependencies Db.Value.self in
@@ -3995,7 +3995,7 @@ stored in the \texttt{b\_extended}\scodeidx{Cil\_types}{behavior}{b\_extended} f
\item A global extension will be found as a global ACSL annotation in the form of a
\sscodeidx{Cil\_types}{global\_annotation}{Dextended}\texttt{Cil\_types.Dextended} constructor.
\item A code annotation extension will be stored with the
-\sscodeidx{Cil\_types}{code\_annotation}{AExtended}\texttt{Cil\_types.AExtended}
+\sscodeidx{Cil\_types}{code\_annotation\_node}{AExtended}\texttt{Cil\_types.AExtended}
constructor. Such an extension has itself
different flavors, determined by the \scodeidx{Cil\_types}{ext\_code\_annot\_context} type:
\begin{itemize}
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 0cb56d772c0423841d1868a58e6914f4509e71af..76bf365de0d1e9064f92f438b68105115f1edfe8 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1527,7 +1527,7 @@ and relation =
| Rle
| Rge
| Req
- | Rneq (** @plugin development guide *)
+ | Rneq (** Different @plugin development guide *)
(** predicates *)
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index be799be80eebc264a562e4ec440385f701c8d841..a28ab252637beaf4ee4f19fdb0db1e30cd4077f5 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -85,9 +85,9 @@ module Lenv : sig
end
-type type_namespace = Typedef | Struct | Union | Enum
(** The different namespaces a C type can belong to, used when we are searching
a type by its name. *)
+type type_namespace = Typedef | Struct | Union | Enum
module Type_namespace: Datatype.S with type t = type_namespace
@@ -132,8 +132,6 @@ type typing_context = {
[typing_context], which allows for open recursion. Namely, it is
possible for the extension to change the type-checking functions for
the sub-nodes of the parsed tree, and not only for the toplevel [lexpr].
-
- @plugin development guide
*)
type_term:
typing_context -> Lenv.t -> Logic_ptree.lexpr -> term;
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index da7d795389d76899763eb37e2670329f8d149f15..a8fb8142af826e6db7b4aa0d3d31ea95372b3950 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -20,12 +20,14 @@
(* *)
(**************************************************************************)
+(** Plugin registration and general services.
+ @plugin development guide
+*)
(** Special signature for Kernel services, whose messages are handled in
an ad'hoc manner. Should not be of any use for a standard plug-in,
who would rather rely on {!Plugin.S} below.
@since Chlorine-20180501
- @plugin development guide
*)
module type S_no_log = sig
@@ -78,7 +80,7 @@ end
@since Beryllium-20090601-beta1
@modify Chlorine-20180501 removed programmatic access to [Debug_category]:
managing categories is now entirely done by Log.Messages
- @plugin development guide *)
+*)
module type S = sig
include Log.Messages
include S_no_log
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 8e32184c6b0679b84784b489ea0cd7d68a0dce33..f2d65db3c320c293209dafe9905047f1084a67a0 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -46,7 +46,7 @@ type 'a ty = 'a t
combination with function {!par} below. *)
type precedence =
| Basic (** Normal precedence @plugin development guide *)
- | Call (** @plugin development guide *)
+ | Call (** Instantiation of polymorphic type @plugin development guide *)
| Tuple
| List
| NoPar
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index d8551183ffe17a263faf75b9e971f34c7c69fc2f..fff461b5b4c57a05323e6d044f3cce741c8e4969 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -225,7 +225,7 @@ val the: exn:exn -> 'a option -> 'a
@modify Magnesium-20151001 add optional argument [exn]
@modify 23.0-Vanadium optional argument [exn] now mandatory; otherwise,
use [Option.get], which is equivalent.
- @plugin development guide *)
+*)
val opt_hash: ('a -> int) -> 'a option -> int
(** @since Sodium-20150201 *)
diff --git a/src/plugins/pdg_types/pdgTypes.mli b/src/plugins/pdg_types/pdgTypes.mli
index e90bc536de1e7316d67addf4c4b3315a866a7426..ca007069dfb42b9b8dee808180aa84873ad72054 100644
--- a/src/plugins/pdg_types/pdgTypes.mli
+++ b/src/plugins/pdg_types/pdgTypes.mli
@@ -22,7 +22,7 @@
(** This module defines the types that are used to store the PDG of a
function.
- @plugin development guide *)
+*)
(** [Dpd] stands for 'dependence'. This object is used as a label on the edges
* of the PDG. There are three kinds of dependencies :
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index 40f1eb7c2d98cca4f390ac3296444570ecbc268d..742d0fd00fa1149cea6030880149fd6a19cb8a75 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-(** @plugin development guide *)
-
include
Plugin.Register
(struct
@@ -30,7 +28,6 @@ include
let help = "function callees"
end)
-(** @plugin development guide *)
module ForceUsers =
False
(struct