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

15 files changed, 72 insertions, 7 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 }