Fix generated titles for the API documentation.

doc/manpages.tex

@@ -345,7 +345,7 @@ A copy of the tools already available in the left toolbar, plus:
   obsolete.
   This allows to replay every proof.
 \item[Non-splitting transformation] applies one of the available
-  transformations, as listed in Section~\ref{sec:transformations}
+  transformations, as listed in Section~\ref{sec:transformations}.
 \item[Splitting transformation] is the same as above, but for
   splitting transformations, \emph{i.e.} those that can generate
   several sub-goals.

src/session/session.mli

@@ -9,11 +9,12 @@
 (*                                                                  *)
 (********************************************************************)
 
-(** Proof sessions *)
-(** Define all the functions needed for managing a session:
-    Creation, saving, loading, modification, ...
-    All the operations are immediately done.
-    Use session_scheduler if you want to queue the operations
+(** Proof sessions
+
+    Define all the functions needed for managing a session:
+    creation, saving, loading, modification, and so on.
+    All the operations are immediately performed.
+    Use session_scheduler if you want to queue operations.
 *)
 
 open Stdlib

src/session/session_scheduler.mli

@@ -9,6 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** Scheduling operations on sessions and calls to provers *)
+
 (*** One module for calling callback when it's time to *)
 module Todo : sig
   type ('a,'b) todo

src/session/session_tools.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-(** This module contains generic tools which can be applied on sessions *)
+(** Generic tools that can be applied on sessions *)
 
 open Session
 
@@ -27,7 +27,7 @@ val convert_unknown_prover : keygen:'a keygen -> 'a env_session -> unit
 val filter_proof_attempt :
   ?notify:'key notify ->
   ('key proof_attempt -> bool) -> 'key session -> unit
-(** remove all the proof attempts which doesn't satisfy the given predicate *)
+(** remove all the proof attempts that do not satisfy the given predicate *)
 
 val transform_proof_attempt :
   ?notify:'key notify ->

src/util/debug.mli

@@ -9,18 +9,19 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** Debug flag handling *)
 
 type flag
 
 val register_flag : desc:Pp.formatted -> string -> flag
-(** Register a new flag. It is allowed to register twice the same flag *)
+(** register a new flag. It is allowed to register twice the same flag *)
 
 val register_info_flag : desc:Pp.formatted -> string -> flag
-(** Register a new info flag. It is allowed to register twice the same flag.
+(** register a new info flag. It is allowed to register twice the same flag.
     Info flags are set by --debug-all and must not change the behaviour. *)
 
 val list_flags : unit -> (string * flag * bool * Pp.formatted) list
-(** List the known flags *)
+(** list the known flags *)
 
 val lookup_flag : string -> flag
 (** get the flag *)

src/util/exthtbl.mli

@@ -9,6 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** Association tables over hashable types *)
+
 val hash : 'a -> int
   (** the same as Hashtbl.hash *)
 

src/util/extmap.mli

@@ -16,7 +16,7 @@
    It is distributed under the terms of its initial license, which
    is provided in the file OCAML-LICENSE. *)
 
-(** Association tables over ordered types.
+(** Association tables over ordered types
 
    This module implements applicative association tables, also known as
    finite maps or dictionaries, given a total ordering function

src/util/extset.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-(** This module extends the standard OCaml Set module. *)
+(** Sets over ordered types *)
 
 (** Input signature of the functor {!Extset.Make}. *)
 module type OrderedType = Set.OrderedType

src/util/lists.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-(* useful list combinators *)
+(** Useful list combinators *)
 
 val rev_map_fold_left :
   ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list

src/util/opt.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-(* useful option combinators *)
+(** Useful option combinators *)
 
 val get : 'a option -> 'a
 

src/util/stdlib.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-(* Set, Map, Hashtbl on ints and strings *)
+(** Specific instances of Set, Map, Hashtbl on int, string, float, and tagged types *)
 
 module Mint : Extmap.S with type key = int
 module Sint : Extset.S with module M = Mint

src/util/strings.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-(* useful function on string *)
+(** Useful functions on string *)
 
 val rev_split : string -> char -> string list