A few other improvements in the API documentation, while I'm at it.

Makefile.in

@@ -1604,9 +1604,7 @@ MODULESTODOC = \
 	driver/whyconf driver/call_provers driver/driver \
 	session/session session/session_tools session/session_scheduler \
 	whyml/mlw_ty whyml/mlw_expr whyml/mlw_decl whyml/mlw_module \
-	whyml/mlw_main
-#	transform/introduction \
-#	ide/db
+	whyml/mlw_wp
 
 FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
 

src/core/env.mli

@@ -9,6 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** {1 Environments} *)
+
 open Stdlib
 
 (** Local type aliases *)
@@ -33,7 +35,7 @@ val create_env : filename list -> env
 val get_loadpath : env -> filename list
 (** returns the loadpath of a given environment *)
 
-(** Input languages *)
+(** {2 Input languages} *)
 
 type 'a language
 
@@ -96,7 +98,7 @@ val list_formats :
     be translated to [lang]. Use [list_formats base_language] to obtain
     the list of all registered formats. *)
 
-(** Language-specific parsers *)
+(** {2 Language-specific parsers} *)
 
 exception InvalidFormat of fformat
 exception UnknownFormat of fformat

src/util/strings.mli

@@ -9,13 +9,15 @@
 (*                                                                  *)
 (********************************************************************)
 
-(** Wrappers for deprecated string functions of OCaml stdlib *)
+(** {1 Additional Useful Functions on Character Strings} *)
+
+(** {2 Wrappers for deprecated string functions of OCaml stdlib} *)
 
 val create : int -> string
 val copy : string -> string
 val set : string -> int -> char -> unit
 
-(** Useful functions on string *)
+(** {2 Other useful functions on strings} *)
 
 val rev_split : char -> string -> string list
 

src/whyml/mlw_decl.mli

@@ -9,13 +9,14 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** {1 Program Declarations} *)
+
 open Ident
 open Term
 open Mlw_ty
 open Mlw_ty.T
 open Mlw_expr
 
-(** *)
 
 (** {2 Type declaration} *)
 

src/whyml/mlw_expr.mli

@@ -9,13 +9,14 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** {1 Program Expressions} *)
+
 open Stdlib
 open Ident
 open Term
 open Mlw_ty
 open Mlw_ty.T
 
-(** *)
 
 (** {2 Program/logic symbols} *)
 

src/whyml/mlw_module.mli

@@ -9,6 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** {1 Program modules} *)
+
 open Stdlib
 open Ident
 open Ty
@@ -20,8 +22,6 @@ open Mlw_ty.T
 open Mlw_expr
 open Mlw_decl
 
-(** *)
-
 type type_symbol =
   | PT of itysymbol
   | TS of tysymbol

src/whyml/mlw_ty.mli

@@ -9,12 +9,12 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** {1 Program Types} *)
+
 open Ident
 open Ty
 open Term
 
-(** *)
-
 (** {2 Individual types (first-order types w/o effects)} *)
 
 module rec T : sig

src/whyml/mlw_wp.mli

@@ -9,13 +9,15 @@
 (*                                                                  *)
 (********************************************************************)
 
+(** {1 Weakest preconditions} *)
+
 open Theory
 open Mlw_ty
 open Mlw_ty.T
 open Mlw_decl
 open Mlw_expr
 
-(** WP-only builtins *)
+(** {2 WP-only builtins} *)
 
 val lemma_label : Ident.label
 
@@ -40,7 +42,7 @@ val remove_old : Term.term -> Term.term
 val full_invariant :
   Decl.known_map -> Mlw_decl.known_map -> Term.vsymbol -> ity -> Term.term
 
-(** Weakest preconditions *)
+(** {2 Weakest precondition computations} *)
 
 val wp_val:
   wp:bool -> Env.env -> known_map -> theory_uc -> let_sym  -> theory_uc
@@ -48,5 +50,3 @@ val wp_let:
   wp:bool -> Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
 val wp_rec:
   wp:bool -> Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
-
-