diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 2de2c65636457199f72c784136cc650ea905cd4e..fa0f3c01ef3fac3fa84bd85314a148cf542217da 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -131,7 +131,7 @@ lexicographic ordering.
 
 For instance, Section \emph{Wished Plug-in} introduces a new sub-section for
 the plug-in \texttt{occurrence} in the following way.
-\codeidxdef{check\_plugin}
+\scodeidxdef{configure.in}{check\_plugin}
 \begin{configurecode}
 # occurrence
 ############
@@ -3994,8 +3994,9 @@ stored in the \texttt{b\_extended}\scodeidx{Cil\_types}{behavior}{b\_extended} f
 \texttt{Cil\_types.behavior}\scodeidx{Cil\_types}{behavior}.
 \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 an
-\scodeidx{Cil\_types}{AExtended}\texttt{Cil\_types.AExtended} constructor. Such an extension has itself
+\item A code annotation extension will be stored with the
+\sscodeidx{Cil\_types}{code\_annotation}{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}
 \item it can be meant to be evaluated exactly at the current program point
diff --git a/doc/developer/check_api/check_and_compare.ml b/doc/developer/check_api/check_and_compare.ml
index 0f80ca36c468055857b3251999616eef4ca41f52..2ba4da64a13fa36ec42c38db0c9aeeb36cc1edf7 100644
--- a/doc/developer/check_api/check_and_compare.ml
+++ b/doc/developer/check_api/check_and_compare.ml
@@ -19,6 +19,23 @@ let index_subentry = Str.regexp {|^.*@\texttt *{\([A-Za-z0-9_]+\)}$|}
 
 let all_caps = Str.regexp "^[A-Z0-9_]+$"
 
+let is_lower s = 'a' <= s.[0] && s.[0] <= 'z'
+let is_upper s = 'A' <= s.[0] && s.[0] <= 'Z'
+
+(* We have a prefix composed of module names, then maybe a lower case
+   symbol, possibly followed by a single symbol (in the case of a
+   type constructor or record field).
+*)
+let is_ocaml_symbol l =
+  let rec aux = function
+    | [] | [_] -> true
+    | [ t; _ ] when is_lower t -> true
+    | x :: l -> is_upper x && aux l
+  in
+  match l with
+  | [] -> false
+  | x :: l -> is_upper x && aux l
+
 let inspect_subentry l =
   let check_one_entry e =
     let e = repair_word e in
@@ -29,7 +46,9 @@ let inspect_subentry l =
   in
   try
     let l = List.map check_one_entry l in
-    (String.concat "." l)  ^ "\n"
+    if is_ocaml_symbol l then
+      (String.concat "." l)  ^ "\n"
+    else ""
   with Exit -> ""
 
 let inspect_entry line =
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 737008eb49d0b27be345c79fef5d151fefa23916..8a6918be6c6daff0b3d79ee223febd7487c2ff39 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -797,7 +797,7 @@ nothing for the other globals.
 \sscodeidx{Cil}{visitAction}{DoChildrenPost}
 \sscodeidx{Cil}{visitAction}{SkipChildren}
 \sscodeidx{Visitor}{frama\_c\_visitor}{vglob\_aux}
-\scodeidx{Cil\_types}{GFun}
+\sscodeidx{Cil\_types}{global}{GFun}
 \scodeidx{Printer\_api}{S.pp\_varinfo}
 
 \texttt{Cil.SkipChildren} tells the visitor not to visit the children
@@ -999,7 +999,7 @@ representing a function definition.
 Now we write the GUI extension code:
 
 \ocamlinput{./tutorial/viewcfg/src/gui.ml}
-\scodeidx{Pretty\_source}{PVDecl}
+\sscodeidx{Pretty\_source}{localizable}{PVDecl}
 \sscodeidx{Globals}{Functions}{get}
 \scodeidx{Kernel\_function}{get\_definition}
 \scodeidx{Dgraph\_helper}{graph\_window}
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 506f932eaf850a6177fd089494b9da91b74e1ea9..0cb56d772c0423841d1868a58e6914f4509e71af 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -143,7 +143,9 @@ and global =
       entire program. Cannot have storage Extern or function type. *)
 
   | GFun of fundec * location
-  (** A function definition. *)
+  (** A function definition.
+      @plugin development guide
+  *)
 
   | GAsm of string * location
   (** Global asm statement. These ones can contain only a template *)
@@ -1694,6 +1696,8 @@ and ext_code_annot_context =
     @since Carbon-20101201 [b_requires] has been added.
     @modify Boron-20100401 [b_ensures] is replaced by [b_post_cond].
     Old [b_ensures] represent the [Normal] case of [b_post_cond].
+
+    @plugin development guide
 *)
 and behavior = {
   mutable b_name : string; (** name of the behavior. *)
@@ -1704,8 +1708,7 @@ and behavior = {
   mutable b_assigns : assigns; (** assignments. *)
   mutable b_allocation : allocation; (** frees, allocates. *)
   mutable b_extended : acsl_extension list
-  (** extensions
-      @plugin development guide *)
+  (** extensions  *)
 }
 
 (** kind of termination a post-condition applies to. See ACSL manual. *)
@@ -1769,7 +1772,10 @@ and code_annotation_node =
   | AExtended of string list * bool * acsl_extension
   (** extension in a code or loop annotation.
       Boolean flag is true for loop extensions and false for code extensions
-      @since Silicon-20161101 *)
+      @since Silicon-20161101
+
+      @plugin development guide
+  *)
 
 (** function contract. *)
 
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e28f890ce5d2ee571f74e0fd23d830695ef25815..be799be80eebc264a562e4ec440385f701c8d841 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -91,7 +91,10 @@ type type_namespace = Typedef | Struct | Union | Enum
 
 module Type_namespace: Datatype.S with type t = type_namespace
 
-(** Functions that can be called when type-checking an extension of ACSL. *)
+(** Functions that can be called when type-checking an extension of ACSL.
+
+    @plugin development guide
+*)
 type typing_context = {
   is_loop: unit -> bool;
   anonCompFieldName : string;
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 31ee2e8af6955160dfa9986ff6aa687ff1a37ddf..02bad2ddd43230e1ef09f63edfd530a27469c4fd 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -286,7 +286,10 @@ module type Hashtbl = sig
 end
 
 (** A datatype for a type [t] extended with predefined set, map and hashtbl
-    over [t]. *)
+    over [t].
+
+    @plugin development guide
+*)
 module type S_with_collections = sig
   include S
   module Set: Set with type elt = t
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 0cc7b1ff57f7b15825f0d3d5345f128eb616e94d..8e32184c6b0679b84784b489ea0cd7d68a0dce33 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -45,7 +45,7 @@ type 'a ty = 'a t
 (** Precedences used for generating the minimal number of parenthesis in
     combination with function {!par} below. *)
 type precedence =
-  | Basic (** @plugin development guide *)
+  | Basic (** Normal precedence @plugin development guide *)
   | Call (** @plugin development guide *)
   | Tuple
   | List
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index 47d055df191824a5b9f2dd30413e873997d7a04b..0b607c99804252b227d5dc062e76376276b58787 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -208,6 +208,7 @@ val register_before_remove_hook: (t -> unit) -> unit
 (* ************************************************************************* *)
 
 exception IOError of string
+(** @plugin development guide *)
 
 val save: ?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit
 (** Save a given project in a file. Default project is [current ()].
diff --git a/src/libraries/stdlib/FCHashtbl.mli b/src/libraries/stdlib/FCHashtbl.mli
index c890d905578e8a781730d37383b94b8b87718a1f..3fe0a74217bc8add3a933a5226ae458c6907c6a9 100644
--- a/src/libraries/stdlib/FCHashtbl.mli
+++ b/src/libraries/stdlib/FCHashtbl.mli
@@ -20,7 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Extension of OCaml's [Hashtbl] module. *)
+(** Extension of OCaml's [Hashtbl] module.
+
+    @plugin development guide
+*)
 
 (* No need to expand OCaml's [Hashtbl.S] here: we do not provide an alternative
    implementation of [Hashtbl]. Hence, we will always be compatible with the
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index a76f237f0cbcc4b53fea9d3bf7e6f9ce16b5beed..5880954f800a2a3940c4b32afca227cc54bb8b9e 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -36,7 +36,10 @@ type localizable = Printer_tag.localizable =
       of the varinfo to distinguish between the various possibilities.
       If the varinfo is a global or a local, the kernel_function is the
       one in which the variable is declared. The [kinstr] argument is given
-      for local variables with an explicit initializer. *)
+      for local variables with an explicit initializer.
+
+      @plugin development guide
+  *)
   | PGlobal of global (** all globals but variable declarations and function
                           definitions. *)
   | PIP of Property.t