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

19 files changed, 171 insertions, 108 deletions

diff --git a/kernel/abstraction.mli b/kernel/abstraction.mli
index 98fd86089..9803b42db 100644
--- a/kernel/abstraction.mli
+++ b/kernel/abstraction.mli
@@ -1,8 +1,12 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
+(*i*)
+
+(* Abstractions. *)
 
 type abstraction_body = { 
   abs_kind : path_kind;
diff --git a/kernel/constant.mli b/kernel/constant.mli
index 7b6589ca5..bc3d1a4e3 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -1,9 +1,13 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Sign
+(*i*)
+
+(* Constants. *)
 
 type discharge_recipe
 
diff --git a/kernel/doc.tex b/kernel/doc.tex
index 2d80109b7..78f1a267d 100644
--- a/kernel/doc.tex
+++ b/kernel/doc.tex
@@ -1,6 +1,9 @@
 
 \section*{The Coq kernel}
 
+\ocwsection 
 This section describes the \Coq\ kernel, which is a type checker for the \CCI.
 
 The modules of the kernel are organized as follows.
+
+TODO
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 34d889897..15b2ca821 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Constant
@@ -8,6 +9,12 @@ open Inductive
 open Evd
 open Univ
 open Sign
+(*i*)
+
+(* Unsafe environments. We define here a datatype for environments. 
+   Since typing is not yet defined, it is not possible to check the
+   informations added in environments, and that is what we speak here
+   of ``unsafe'' environments. *)
 
 type 'a unsafe_env
 
@@ -50,6 +57,10 @@ val is_existential : constr -> bool
 
 val mind_nparams : 'a unsafe_env -> constr -> int
 
+(*s Unsafe judgments. We introduce here the pre-type of judgments, which is
+  actually only a datatype to store a term with its type and the type of its
+  type. *)
+
 type unsafe_judgment = { 
   uj_val : constr;
   uj_type : constr;
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 40006fdf9..dcd458f8b 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -6,6 +6,8 @@ open Util
 open Names
 (*i*)
 
+(* A generic notion of terms with binders. *)
+
 exception FreeVar
 exception Occur
 
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 20a0adfc1..8723ec3c6 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -1,8 +1,10 @@
 
 (* $Id$ *)
 
+(*i*)
 open Inductive
 open Environ
+(*i*)
 
 (* [mind_check_arities] checks that the types declared for all the
    inductive types are some arities. *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c60c3cf4e..a08136424 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,9 +1,11 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Sign
+(*i*)
 
 (* Inductive types (internal representation). *)
 
@@ -74,10 +76,21 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
+(* [mind_check_names] checks the names of an inductive types declaration
+   i.e. that all the types and constructors names are distinct. 
+   It raises an exception [InductiveError _] if it is not the case. *)
+
 val mind_check_names : mutual_inductive_entry -> unit
 
-val mind_extract_params : int -> constr -> (name * constr) list * constr
+(* [mind_extract_and_check_params] extracts the parameters of an inductive
+   types declaration. It raises an exception [InductiveError _] if there is
+   not enough abstractions in any of the terms of the field 
+   [mind_entry_inds]. *)
+
 val mind_extract_and_check_params : 
   mutual_inductive_entry -> (name * constr) list
 
+val mind_extract_params : int -> constr -> (name * constr) list * constr
+
+
 val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index e0279abb1..0bcdabf6d 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -1,9 +1,13 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Environ
+(*i*)
+
+(* Instantiation of constants and inductives on their real arguments. *)
 
 val instantiate_constr : 
   identifier list -> constr -> constr list -> constr
diff --git a/kernel/names.mli b/kernel/names.mli
index 6968d7b96..e5c5ad0f4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -5,6 +5,8 @@
 open Pp
 (*i*)
 
+(* Names. *)
+
 type identifier
 type name = Name of identifier | Anonymous
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 0f53d600b..c9cafccec 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -148,7 +148,7 @@ type 'a conversion_function =
 
 val fconv : conv_pb -> 'a conversion_function
 
-(* fconv has 2 instances:
+(* [fconv] has 2 instances:
    \begin{itemize}
    \item [conv = fconv CONV] : 
      conversion test, and adjust universes constraints
diff --git a/kernel/sign.mli b/kernel/sign.mli
index c9e1fb565..092e5c078 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,6 +7,8 @@ open Generic
 open Term
 (*i*)
 
+(* Signatures (with named and de Bruijn variables). *)
+
 type 'a signature = identifier list * 'a list
 type 'a db_signature = (name * 'a) list
 type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
diff --git a/kernel/sosub.mli b/kernel/sosub.mli
index c3093af73..531b7ee7e 100644
--- a/kernel/sosub.mli
+++ b/kernel/sosub.mli
@@ -1,7 +1,11 @@
 
 (* $Id$ *)
 
+(*i*)
 open Term
+(*i*)
+
+(* Second-order substitutions. *)
 
 val soexecute : constr -> constr
 val try_soexecute : constr -> constr
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 76bf18cc3..3a3e1488e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -1,11 +1,13 @@
 
 (* $Id$ *)
 
+(*i*)
 open Pp
 open Names
 open Term
 open Sign
 open Environ
+(*i*)
 
 (* Type errors. *)
 
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 0b236ce44..b9ef2893a 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -249,6 +249,9 @@ let lookup_mind = lookup_mind
 let lookup_mind_specif = lookup_mind_specif
 let lookup_meta = lookup_meta
 
+(* Insertion of variables (named and de Bruijn'ed). They are now typed before
+   being added to the environment. *)
+
 let push_rel_or_var push (id,c) env =
   let (j,u) = safe_machine env c in
   let env' = set_universes u env in
@@ -259,6 +262,14 @@ let push_var nvar env = push_rel_or_var push_var nvar env
 
 let push_rel nrel env = push_rel_or_var push_rel nrel env
 
+let push_vars vars env =
+  List.fold_left (fun env nvar -> push_var nvar env) env vars
+
+let push_rels vars env =
+  List.fold_left (fun env nvar -> push_rel nvar env) env vars
+
+(* Insertion of constants and parameters in environment. *)
+
 let add_constant sp ce env =
   let (jb,u) = safe_machine env ce.const_entry_body in
   let env' = set_universes u env in
@@ -294,11 +305,7 @@ let add_parameter sp c env =
   in
   Environ.add_constant sp cb env'
 
-let push_vars vars env =
-  List.fold_left (fun env nvar -> push_var nvar env) env vars
-
-let push_rels vars env =
-  List.fold_left (fun env nvar -> push_rel nvar env) env vars
+(* Insertion of inductive types. *)
 
 let check_type_constructs env_params univ nparams lc =
   let check_one env c =
@@ -334,6 +341,7 @@ let add_mind sp mie env =
 
 type judgment = unsafe_judgment
 
+
 (*s Machines with information. *)
 
 type information = Logic | Inf of unsafe_judgment
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1b47e00b4..b262ad718 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -1,7 +1,11 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
+(*i*)
+
+(* Universes. *)
 
 type universe = { u_sp : section_path; u_num : int }
 
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