From c985e7b0ac31ab987f4bb0bd14662146c8f06c6a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 1 Jun 2022 17:57:28 +0200
Subject: [PATCH] [devguide] Fix last discrepancies between OCamldoc and LaTeX
index
---
doc/developer/advance.tex | 6 +++---
src/kernel_services/ast_data/cil_types.mli | 2 +-
src/kernel_services/ast_queries/logic_typing.mli | 4 +---
src/kernel_services/plugin_entry_points/plugin.mli | 6 ++++--
src/libraries/datatype/type.mli | 2 +-
src/libraries/stdlib/extlib.mli | 2 +-
src/plugins/pdg_types/pdgTypes.mli | 2 +-
src/plugins/users/users_register.ml | 3 ---
8 files changed, 12 insertions(+), 15 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index fa0f3c01ef3..2411abb40fa 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 0cb56d772c0..76bf365de0d 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 be799be80ee..a28ab252637 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 da7d795389d..a8fb8142af8 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 8e32184c6b0..f2d65db3c32 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 d8551183ffe..fff461b5b4c 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 e90bc536de1..ca007069dfb 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 40f1eb7c2d9..742d0fd00fa 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
--
GitLab