un petit effort de presentation dans les interfaces

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 99 insertions, 101 deletions

diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 76a8fba4e..917c063e1 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -1,19 +1,9 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                               hashcons.mli                               *)
-(****************************************************************************)
-val stat: unit->unit
 
+(* $Id$ *)
+
+(* Generic hash-consing. *)
+
+val stat : unit->unit
 
 module type Comp =
   sig
@@ -31,7 +21,7 @@ module type S =
     val f : unit -> (u -> t -> t)
   end
 
-module Make(X:Comp): (S with type t = X.t and type u = X.u)
+module Make(X:Comp) : (S with type t = X.t and type u = X.u)
 
 val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
 val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
@@ -42,12 +32,11 @@ val recursive2_hcons :
     (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
       'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
 
-
 (* Declaring and reinitializing global hash-consing functions *)
+
 val init : unit -> unit
 val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
 
-
 module Hstring : (S with type t = string and type u = unit)
 module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
 
@@ -56,5 +45,3 @@ val obj : Obj.t -> Obj.t
 
 val magic_hash : 'a -> 'a
 
-(* $Id$ *)
-
diff --git a/lib/pp.mli b/lib/pp.mli
index 62f402a9b..c4600fcdf 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -5,77 +5,86 @@
 open Pp_control
 (*i*)
 
+(* Pretty-printers. *)
+
 type 'a ppcmd_token
 
 type std_ppcmds = (int*string) ppcmd_token Stream.t
 
-(* formatting commands *)
-val sTR  : string -> (int*string) ppcmd_token (* string *)
+(*s Formatting commands. *)
+
+val sTR  : string -> (int*string) ppcmd_token
 val sTRas : int * string -> (int*string) ppcmd_token
-                                              (* string with length *)
-val bRK  : int * int -> 'a ppcmd_token        (* break *)
-val tBRK : int * int -> 'a ppcmd_token        (* go to tabulation *)
-val tAB  : 'a ppcmd_token                     (* set tabulation *)
-val fNL  : 'a ppcmd_token                     (* force newline *)
-val pifB : 'a ppcmd_token                     (* print if broken *)
-val wS   : int -> 'a ppcmd_token              (* white space *)
-
-(* derived commands *)
-val sPC     : 'a ppcmd_token                        (* space *)
-val cUT     : 'a ppcmd_token                        (* cut *)
-val aLIGN   : 'a ppcmd_token                        (* go to tab *)
-val iNT     : int -> (int*string) ppcmd_token       (* int *)
-val rEAL    : float -> (int * string) ppcmd_token   (* real *)
-val bOOL    : bool -> (int * string) ppcmd_token    (* bool *)
-val qSTRING : string -> (int * string) ppcmd_token  (* quoted string *)
-val qS      : string -> (int * string) ppcmd_token  (*   "       "   *)
-
-(* boxing commands *)
-val h   : int -> std_ppcmds -> std_ppcmds (* H box   *) 
-val v   : int -> std_ppcmds -> std_ppcmds (* V box   *)
-val hV  : int -> std_ppcmds -> std_ppcmds (* HV box  *)  
-val hOV : int -> std_ppcmds -> std_ppcmds (* HOV box *)
-val t   : std_ppcmds -> std_ppcmds        (* TAB box *)
-
-(* Opening and closing of boxes *)
-val hB    : int -> 'a ppcmd_token  (* open hbox *)
-val vB    : int -> 'a ppcmd_token  (* open vbox *)
-val hVB   : int -> 'a ppcmd_token  (* open hvbox *)
-val hOVB  : int -> 'a ppcmd_token  (* open hovbox *)
-val tB    : 'a ppcmd_token         (* open tbox *)
-val cLOSE : 'a ppcmd_token         (* close box *)
-val tCLOSE: 'a ppcmd_token         (* close tbox *)
-
-
-(* pretty printing functions WITHOUT FLUSH *)
-val pP_with       : Format.formatter -> std_ppcmds -> unit
-val pPNL_with     : Format.formatter -> std_ppcmds -> unit
-val warning_with  : Format.formatter -> string -> unit
-val wARN_with     : Format.formatter -> std_ppcmds -> unit
+val bRK : int * int -> 'a ppcmd_token
+val tBRK : int * int -> 'a ppcmd_token
+val tAB : 'a ppcmd_token
+val fNL : 'a ppcmd_token
+val pifB : 'a ppcmd_token
+val wS : int -> 'a ppcmd_token
+
+(*s Derived commands. *)
+
+val sPC : 'a ppcmd_token
+val cUT : 'a ppcmd_token
+val aLIGN : 'a ppcmd_token
+val iNT : int -> (int*string) ppcmd_token
+val rEAL : float -> (int * string) ppcmd_token
+val bOOL : bool -> (int * string) ppcmd_token
+val qSTRING : string -> (int * string) ppcmd_token
+val qS : string -> (int * string) ppcmd_token
+
+(*s Boxing commands. *)
+
+val h : int -> std_ppcmds -> std_ppcmds
+val v : int -> std_ppcmds -> std_ppcmds
+val hV : int -> std_ppcmds -> std_ppcmds
+val hOV : int -> std_ppcmds -> std_ppcmds
+val t : std_ppcmds -> std_ppcmds
+
+(*s Opening and closing of boxes. *)
+
+val hB : int -> 'a ppcmd_token
+val vB : int -> 'a ppcmd_token
+val hVB : int -> 'a ppcmd_token
+val hOVB : int -> 'a ppcmd_token
+val tB : 'a ppcmd_token
+val cLOSE : 'a ppcmd_token
+val tCLOSE : 'a ppcmd_token
+
+(*s Pretty-printing functions WITHOUT FLUSH. *)
+
+val pP_with : Format.formatter -> std_ppcmds -> unit
+val pPNL_with : Format.formatter -> std_ppcmds -> unit
+val warning_with : Format.formatter -> string -> unit
+val wARN_with : Format.formatter -> std_ppcmds -> unit
 val pp_flush_with : Format.formatter -> unit -> unit
 
-(* pretty printing functions WITH FLUSH *)
-val mSG_with      : Format.formatter -> std_ppcmds -> unit
-val mSGNL_with    : Format.formatter -> std_ppcmds -> unit
+(*s Pretty-printing functions WITH FLUSH. *)
+
+val mSG_with : Format.formatter -> std_ppcmds -> unit
+val mSGNL_with : Format.formatter -> std_ppcmds -> unit
 
 
-(* These are instances of the previous ones on [std_ft] and [err_ft] *)
+(*s The following functions are instances of the previous ones on
+  [std_ft] and [err_ft]. *)
 
-(* pretty printing functions WITHOUT FLUSH on stdout and stderr *)
-val pP       : std_ppcmds -> unit
-val pPNL     : std_ppcmds -> unit
-val pPERR    : std_ppcmds -> unit
-val pPERRNL  : std_ppcmds -> unit
-val message  : string -> unit       (* = pPNL *)
-val warning  : string -> unit
-val wARN     : std_ppcmds -> unit
+(*s Pretty-printing functions WITHOUT FLUSH on [stdout] and [stderr]. *)
+
+val pP : std_ppcmds -> unit
+val pPNL : std_ppcmds -> unit
+val pPERR : std_ppcmds -> unit
+val pPERRNL : std_ppcmds -> unit
+val message : string -> unit       (* = pPNL *)
+val warning : string -> unit
+val wARN : std_ppcmds -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(* pretty printing functions WITH FLUSH on stdout and stderr *)
-val mSG      : std_ppcmds -> unit
-val mSGNL    : std_ppcmds -> unit
-val mSGERR   : std_ppcmds -> unit
+(*s Pretty-printing functions WITH FLUSH on [stdout] and [stderr]. *)
+
+val mSG : std_ppcmds -> unit
+val mSGNL : std_ppcmds -> unit
+val mSGERR : std_ppcmds -> unit
 val mSGERRNL : std_ppcmds -> unit
-val wARNING  : std_ppcmds -> unit
+val wARNING : std_ppcmds -> unit
 
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 03a1487bf..6c92849a7 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -1,7 +1,7 @@
 
 (* $Id$ *)
 
-(* Parameters of pretty-printing *)
+(* Parameters of pretty-printing. *)
 
 type pp_global_params = { 
   margin : int;
@@ -9,30 +9,31 @@ type pp_global_params = {
   max_depth : int;
   ellipsis : string }
 
-val dflt_gp : pp_global_params                (* default parameters *)
-val deep_gp : pp_global_params                (* with depth = 10000 *)
+val dflt_gp : pp_global_params
+val deep_gp : pp_global_params
 val set_gp : Format.formatter -> pp_global_params -> unit
 val set_dflt_gp : Format.formatter -> unit
 val get_gp : Format.formatter -> pp_global_params
 
 
-(* Output functions of pretty-printing *)
+(*s Output functions of pretty-printing. *)
 
-type 'a pp_formatter_params ={ 
-  fp_output : out_channel ;
-  fp_output_function : string -> int -> int -> unit ;
+type 'a pp_formatter_params = { 
+  fp_output : out_channel;
+  fp_output_function : string -> int -> int -> unit;
   fp_flush_function : unit -> unit }
 
-val std_fp : (int*string) pp_formatter_params (* output functions for stdout *)
-val err_fp : (int*string) pp_formatter_params (* output functions for stderr *)
+val std_fp : (int*string) pp_formatter_params
+val err_fp : (int*string) pp_formatter_params
 
 val with_fp : 'a pp_formatter_params -> Format.formatter
 val with_output_to : out_channel -> Format.formatter
 
-val std_ft : Format.formatter  (* the formatter on stdout *)
-val err_ft : Format.formatter  (* the formatter on stderr *)
-val deep_ft : Format.formatter (* a deep formatter on stdout (depth=10000) *)
+val std_ft : Format.formatter
+val err_ft : Format.formatter
+val deep_ft : Format.formatter
+
+(*s For parametrization through vernacular. *)
 
-(* For parametrization through vernacular *)
 val set_depth_boxes : int -> unit
 val get_depth_boxes : unit -> int
diff --git a/lib/util.mli b/lib/util.mli
index 0faf3f290..9517d8742 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -5,24 +5,25 @@
 open Pp
 (*i*)
 
-(* Errors *)
+(* Errors. [Anomaly] is used for system errors and [UserError] for the
+   user's ones. *)
 
-exception Anomaly of string * std_ppcmds  (* System errors *)
+exception Anomaly of string * std_ppcmds
 val anomaly : string -> 'a
 val anomalylabstrm : string -> std_ppcmds -> 'a
 
-exception UserError of string * std_ppcmds (* User errors *)
+exception UserError of string * std_ppcmds
 val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
 
-(* Strings *)
+(*s Strings. *)
 
 val explode : string -> string list
 val implode : string list -> string
 
 val parse_section_path : string -> string list * string * string
 
-(* Lists *)
+(*s Lists. *)
 
 val list_intersect : 'a list -> 'a list -> 'a list
 val list_unionq : 'a list -> 'a list -> 'a list
@@ -37,7 +38,7 @@ val list_index : 'a -> 'a list -> int
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 
-(* Arrays *)
+(*s Arrays. *)
 
 val array_exists : ('a -> bool) -> 'a array -> bool
 val array_for_all : ('a -> bool) -> 'a array -> bool
@@ -58,18 +59,18 @@ val array_map_to_list : ('a -> 'b) -> 'a array ->'b list
 val array_chop : int -> 'a array -> 'a array * 'a array
 val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 
-(* Functions *)
+(*s Functions. *)
 
 val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
 val iterate : ('a -> 'a) -> int -> 'a -> 'a
 
-(* Misc *)
+(*s Misc. *)
 
 type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
 
-(* Pretty-printing *)
+(*s Pretty-printing. *)
 
 val pr_spc : unit -> std_ppcmds
 val pr_fnl : unit -> std_ppcmds