diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index fed8733f54f0271617cd944e3c23bb3698af4840..8b0194251b24916a55f9511cf2bac97d2b97c126 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -759,7 +759,7 @@ class registerLabelsVisitor : cilVisitor = object
   method! vattr _ = Cil.SkipChildren (* via block stmt *)
 end
 
-(* prepare a function for computeCFGInfo by removing break, continue,
+(* prepare a function for cfgFun by removing break, continue,
  * default and switch statements/labels and replacing them with Ifs and
  * Gotos. *)
 let prepareCFG ?(keepSwitch=false) (fd : fundec) : unit =
diff --git a/src/kernel_internals/typing/cfg.mli b/src/kernel_internals/typing/cfg.mli
index 0cc33e231128e5812b91e775be881bc2885dadfe..b040cda0b17bf99457fdfd0725c04cec53965e1e 100644
--- a/src/kernel_internals/typing/cfg.mli
+++ b/src/kernel_internals/typing/cfg.mli
@@ -42,14 +42,15 @@
 (****************************************************************************)
 
 (** Code to compute the control-flow graph of a function or file.
-    This will fill in the [preds] and [succs] fields of {!Cil.stmt}
+    This will fill in the [preds] and [succs] fields of {!Cil_types.stmt}
 
     This is nearly always automatically done by the kernel. You only need
     those functions if you build {!Cil_types.fundec} yourself. *)
 
 open Cil_types
 
-(** Compute the CFG for an entire file, by calling cfgFun on each function. *)
+(** Compute the CFG for an entire file,
+    by calling {!cfgFun} on each function. *)
 val computeFileCFG: file -> unit
 
 (** clear the sid (except when clear_id is explicitly set to false),
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index ee17c45ca945d38a6dadc0b414b1982eb6eb7209..edc20ab1911ee5502ca23103d431e745250d2d99 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -205,7 +205,7 @@ val fold_int_decrease : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
     potentially infinite integer. *)
 
 val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a
-(** Iterate on every value of the ival. Raise {!Abstract_intrep.Error_Top} if
+(** Iterate on every value of the ival. Raise {!Abstract_interp.Error_Top} if
     the argument is a non-singleton float or a potentially infinite integer. *)
 
 val fold_int_bounds: (t -> 'a -> 'a) -> t -> 'a -> 'a
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index db5f8475e6ad128609468f8db9bca79e5b2d1b0f..cb163f4f158eb66fcc1a3d1bb1cf6ab61fab7854 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -142,8 +142,8 @@ module Location_Bytes : sig
   (** [fold_enum f loc acc] enumerates the locations in [acc], and passes
       them to [f]. Make sure to call {!cardinal_less_than} before calling
       this function, as all possible combinations of bases/offsets are
-      presented to [f]. Raises {!Error_Top} if [loc] is [Top _] or if
-      one offset cannot be enumerated. *)
+      presented to [f]. Raises {!Abstract_interp.Error_Top} if [loc] is
+      [Top _] or if one offset cannot be enumerated. *)
 
   val to_seq_i : t -> (Base.t * Ival.t) Seq.t
   (** Builds a sequence of all bases (with their offsets) of the location.
diff --git a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml
index 8006e51fb8750bb76205bc605dcf67da488c480a..f6c967019b580847097512aa51c3a757b56d02cd 100644
--- a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml
+++ b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml
@@ -53,8 +53,8 @@ module type S = sig
     start:Integer.t -> stop:Integer.t -> size:Integer.t ->
     t ->
     bool * t
-  (** Extract the bits between {!start} and {!stop} in the value of type [t],
-      assuming this value has {!size} bits. Return the corresponding value, and
+  (** Extract the bits between [start] and [stop] in the value of type [t],
+      assuming this value has [size] bits. Return the corresponding value, and
       a boolean indicating that an imprecision occurred during the operation.
       In the latter case, the origin of the imprecision is flagged as having kind
       [topify]. *)
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index d603249ae2e308282a4f99c8a8e619c36ea3f7b9..f336d1619d6d221ed2c036ee0ccfea1f1dd0a517 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -79,8 +79,7 @@ type file = {
   (** An optional global initializer function. This is a function where you
       can put stuff that must be executed before the program is
       started. This function, is conceptually at the end of the file,
-      although it is not part of the globals list. Use {!Cil.getGlobInit} to
-      create/get one. *)
+      although it is not part of the globals list. *)
 
   mutable globinitcalled: bool;
   (** Whether the global initialization function is called in main. This
@@ -180,7 +179,7 @@ and global =
     CIL is configured at build-time with the sizes and alignments of the
     underlying compiler (GCC or MSVC). CIL contains functions that can compute
     the size of a type (in bits) {!Cil.bitsSizeOf}, the alignment of a type (in
-    bytes) {!Cil.alignOf_int}, and can convert an offset into a start and width
+    bytes) {!Cil.bytesAlignOf}, and can convert an offset into a start and width
     (both in bits) using the function {!Cil.bitsOffset}. At the moment these
     functions do not take into account the [packed] attributes and pragmas. *)
 
@@ -333,12 +332,13 @@ and attrparam =
     Constructing a {!Cil_types.compinfo} can be tricky since it must contain
     fields that might refer to the host {!Cil_types.compinfo} and furthermore
     the type of the field might need to refer to the {!Cil_types.compinfo} for
-    recursive types.  Use the {!Cil.mkCompInfo} function to create a
+    recursive types.  Use the {!Cil_const.mkCompInfo} function to create a
     {!Cil_types.compinfo}. You can easily fetch the {!Cil_types.fieldinfo} for a
     given field in a structure with {!Cil.getCompField}. *)
 
-(** The definition of a structure or union type. Use {!Cil.mkCompInfo} to make
-    one and use {!Cil.copyCompInfo} to copy one (this ensures that a new key is
+(** The definition of a structure or union type. Use {!Cil_const.mkCompInfo} to
+    make one and use {!Cil_const.copyCompInfo} to copy one (this ensures that
+    a new key is
     assigned and that the fields have the right pointers to parents.).
     @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
 *)
@@ -964,10 +964,10 @@ and fundec = {
   mutable smaxstmtid: int option;
   (** max id of a (reachable) statement in this function, if we have
       computed it. range = 0 ...  (smaxstmtid-1). This is computed by
-      {!Cfg.computeCFGInfo}. *)
+      {!Cfg.cfgFun}. *)
 
   mutable sallstmts: stmt list;
-  (** After you call {!Cfg.computeCFGInfo} this field is set to contain all
+  (** After you call {!Cfg.cfgFun} this field is set to contain all
       statements in the function. *)
 
   mutable sspec: funspec;
@@ -1019,8 +1019,8 @@ and block = {
     [stmt] can be used to give unique numbers to statements, and the [succs] and
     [preds] fields can be used to maintain a list of successors and predecessors
     for every statement. The CFG information is not computed by default. Instead
-    you must explicitly use the functions {!Cfg.prepareCFG} and
-    {!Cfg.computeCFGInfo} to do it. *)
+    you must explicitly use functions {!Cfg.prepareCFG} and {!Cfg.cfgFun}
+    to do it. *)
 
 (** Statements.
     @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index a2419446a6213020bb3faa8bbac10e320e46a275..3dabf90e2ddf04f36261001d804ca8500d777284 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -214,7 +214,7 @@ class type extensible_printer_type = object
   (** Print a statement kind. The code to be printed is given in the
       {!Cil_types.stmtkind} argument.  The initial {!Cil_types.stmt} argument
       records the statement which follows the one being printed;
-      {!defaultCilPrinterClass} uses this information to prettify statement
+      {!Printer.extensible_printer} uses this information to prettify statement
       printing in certain special cases. The boolean flag indicated whether
       the statement has labels (which have already been printed) *)
 
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 17cda409b1b1f02caf111ddbb60e3e3d0b4915cb..97b5b40eef895dbe324e1f12658f6b34bb770829 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2097,7 +2097,7 @@ val visitCilFile: cilVisitor -> file -> unit
     @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
 val visitCilFileSameGlobals: cilVisitor -> file -> unit
 
-(** Same as {!visitCilFilesSameGlobals}, but only visits function definitions
+(** Same as {!Cil.visitCilFileSameGlobals}, but only visits function definitions
     (i.e. behaves as if all globals but [GFun] return [SkipChildren]).
     @since 25.0-Manganese
 *)
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index b0da114f710eb07aa892549ae92e31cd826a4a98..d3d89a240a9dac900ec0be036a0c4814090e0a8d 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -186,7 +186,7 @@ val create_project_from_visitor:
     [true] (by default), remember than the returned project is the last
     created one.
     The visitor is responsible to avoid sharing between old file and new
-    file (i.e. it should use {!Cil.copy_visit} at some point).
+    file (i.e. it should use {!Visitor_behavior.copy} at some point).
     @raise File_types.Bad_Initialization if called more than once.
     @since Beryllium-20090601-beta1
     @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
@@ -197,7 +197,7 @@ val create_rebuilt_project_from_visitor:
 (** Like {!create_project_from_visitor}, but the new generated cil file is
     generated into a temp .i or .c file according to [preprocess], then re-built
     by Frama-C in the returned project. For instance, use this function if the
-    new cil file contains a constructor {!GText} as global.
+    new cil file contains a constructor {!Cil_types.GText} as global.
 
     Note that the generation of a preprocessed C file may fail in some cases
     (e.g. if it includes headers already included). Thus the generated file is
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index 37bbd37b1881f171ce260125c89da7d8b44af7c1..efbcc9e79146abc00a92f21ec339423bfee97242 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -169,7 +169,7 @@ val remove_logic_function: string -> unit
     Otherwise, does nothing if no logic info with the same profile as [li]
     is in the table.
 
-    See {!Logic_env.add_logic_info_gen} for more information about the
+    See {!Logic_env.add_logic_function_gen} for more information about the
     [is_same_profile] argument.
 
     @since Chlorine-20180501
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 8ab9618a28e2b85de0278a8a57e59387440a5c95..2897ada6e381c16a59e38b96b3150f3b8bfbc02a 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -145,12 +145,6 @@ val numeric_coerce: logic_type -> term -> term
 
 (** {2 Predicates} *)
 
-(** \valid_index *)
-(* val mk_pvalid_index: ?loc:location -> term * term -> predicate *)
-
-(** \valid_range *)
-(* val mk_pvalid_range: ?loc:location -> term * term * term -> predicate *)
-
 val pointer_comparable:
   ?loc:location -> ?label:logic_label -> term -> term -> predicate
 (** \pointer_comparable. [label] defaults to {!Logic_const.here_label}
@@ -448,9 +442,9 @@ val use_predicate : predicate_kind -> bool
     It is true for `Assert` and `Check`, and false for `Admit`. *)
 val verify_predicate : predicate_kind -> bool
 
-(** Functions below allows to test a special kind of code_annotation.
-    Use them in conjunction with {!Annotations.get_filter} to retrieve
-    a particular kind of annotations associated to a statement. *)
+(** The functions below allow testing for specific kinds of [code_annotation].
+    Use them in conjunction with iterators in {!Annotations} to retrieve
+    a particular kind of annotation associated to a statement. *)
 
 val is_assert : code_annotation -> bool
 val is_check : code_annotation -> bool
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index ff51d3e0f5b15023c5b7e1fd665756a7f5c85313..8f798e1476f7bffab2f543cdf8be6fb1b3cddaac 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -28,7 +28,7 @@
    - {!Dynamic}: API for plug-ins linked dynamically
    - {!Log}: message outputs and printers
    - {!Plugin}: general services for plug-ins
-   - {!Project} and associated files: {!Kind}, {!Datatype} and {!State_builder}.
+   - {!Project} and associated files: {!Datatype} and {!State_builder}.
 
    Other main kernel modules:
    - {!Ast}: the cil AST
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index a2017f9fede5bbc264d67c908977de5c3b6e3f5b..9743f1b354029a53ef5deec96c405ed1a125b72c 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -159,7 +159,7 @@ val create_by_copy:
     the copy function of the copied state is implemented. All the hooks
     applied when loading a project are applied (see {!load}).
     If [last], then remember that the returned project is the last created
-    one (see {!last_created_by_copy}).
+    one.
 *)
 
 val create_by_copy_hook: (t -> t -> unit) -> unit
@@ -170,7 +170,7 @@ val create_by_copy_hook: (t -> t -> unit) -> unit
 val clear: ?selection:State_selection.t -> ?project:t -> unit -> unit
 (** Clear the given project. Default project is [current ()]. All the
     internal states of the given project are now empty (wrt the action
-    registered with {!register_todo_on_clear}).
+    registered with {!register_todo_before_clear}).
     @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
 
 val register_todo_before_clear: (t -> unit) -> unit
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index ac53d7d75c780c7fde1eb1f6c52cd9125c9424b5..edf54150e1d077b84a7fccddf386d7962946301a 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -214,7 +214,7 @@ module type Weak_hashtbl = sig
   include S
   (** Hashtbl are a standard computation.
       BUT it is INCORRECT to use projectified hashtables if keys have a
-      custom [rehash] function (see {!Project.DATATYPE_OUTPUT.rehash}) *)
+      custom [rehash] function (see {!Datatype.Make_input.rehash}) *)
 
   type data
   (** @since Boron-20100401 *)
@@ -321,7 +321,7 @@ module Hashconsing_tbl: Hashconsing_tbl
 (** {3 Hashtables}
 
     IMPORTANT: that is INCORRECT to use projectified hashtables if keys have a
-    custom [rehash] function (see {!Project.DATATYPE_OUTPUT.rehash}) *)
+    custom [rehash] function (see {!Datatype.Make_input.rehash}) *)
 (* ************************************************************************* *)
 
 (** Events emitted when an [Hashtbl] state changes. *)
@@ -338,7 +338,7 @@ module type Hashtbl = sig
   include S
   (** Hashtbl are a standard computation.
       BUT that is INCORRECT to use projectified hashtables if keys have a
-      custom [rehash] function (see {!Project.DATATYPE_OUTPUT.rehash}) *)
+      custom [rehash] function (see {!Datatype.Make_input.rehash}) *)
 
   type key
   type data
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.mli b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
index ba20ba0ed37a395fe0fa795d145bdf5f3ff45bff..d66ae805534b9ba2d4cc9803273df12f9b31b239 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.mli
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
@@ -32,15 +32,15 @@ val use_monitoring: unit -> bool
 (** Is one variable monitored (at least)? *)
 
 val must_monitor_vi: ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
-(** [must_model_vi ?kf ?stmt vi] returns [true] if the varinfo [vi] at the given
+(** [must_monitor_vi ?kf ?stmt vi] returns [true] if the varinfo [vi] at the given
     [stmt] in the given function [kf] must be tracked by the memory model
     library. *)
 
 val must_monitor_lval: ?kf:kernel_function -> ?stmt:stmt -> lval -> bool
-(** Same as {!must_model_vi}, for left-values *)
+(** Same as {!must_monitor_vi}, for left-values *)
 
 val must_monitor_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
-(** Same as {!must_model_vi}, for expressions *)
+(** Same as {!must_monitor_vi}, for expressions *)
 
 val found_concurrent_function: loc:location -> varinfo -> unit
 (** [found_concurrent_function ~loc fvi] signals to the memory tracking
diff --git a/src/plugins/pdg/api.mli b/src/plugins/pdg/api.mli
index ac57bccef3e3d3649f12f5dcddf771841b88ff47..1b955222eb12bdb99dc32c7834985fb5cd1c2f99 100644
--- a/src/plugins/pdg/api.mli
+++ b/src/plugins/pdg/api.mli
@@ -62,7 +62,7 @@ val from_same_fun : t -> t -> bool
 
 (**************************************************************************)
 
-(** {Finding PDG nodes} *)
+(** {3 Finding PDG nodes} *)
 
 val find_decl_var_node : t -> Cil_types.varinfo -> PdgTypes.Node.t
 (** Get the node corresponding the declaration of a local variable or a
diff --git a/src/plugins/pdg/ctrlDpds.mli b/src/plugins/pdg/ctrlDpds.mli
index 9d17c613976b14465203b581db8e21f77f83f277..cf60f114ed2fd1e8a501549d62181cf02ad38101 100644
--- a/src/plugins/pdg/ctrlDpds.mli
+++ b/src/plugins/pdg/ctrlDpds.mli
@@ -34,7 +34,7 @@ val get_if_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
 (** Compute the list of the statements that should have a control dependency
  * on the given jump statement. This statement can be a [goto] of course,
  * but also a [break], a [continue], or even a loop because CIL transformations
-    make them of the form {v while(true) body; v} which is equivalent to
+    make them of the form [while(true) body;] which is equivalent to
     [L : body ; goto L;]
  * *)
 val get_jump_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t
diff --git a/src/plugins/pdg/marks.mli b/src/plugins/pdg/marks.mli
index 66222d479950e62405e8488b0a84aeee7a68326b..34ca2126defffd84ce8e24cfd07f3d4fcfe6a199 100644
--- a/src/plugins/pdg/marks.mli
+++ b/src/plugins/pdg/marks.mli
@@ -31,7 +31,7 @@ open PdgMarks
     So this function takes one call to [f] and translate input keys into nodes.
 
     The function ([m2m]) is called for each element to translate.
-    See {!m2m} for more information about how to use it. *)
+    See {!PdgMarks.m2m} for more information about how to use it. *)
 val in_marks_to_caller :
   PdgTypes.Pdg.t ->
   Cil_types.stmt ->