documentation

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

7 files changed, 14 insertions, 13 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 2b68faa0c8..f01ce7d732 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -63,12 +63,10 @@ val mis_consnames : mind_specif -> identifier array
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
 
-(* A light version of [mind_specif_of_mind] with pre-splitted args
-   Invariant: We have
-
-   -- [Hnf (fullmind)] = [DOPN(AppL,[|MutInd mind;..params..;..realargs..|])]
-
-   with [mind]  = [((sp,i),localvars)] for some [sp, i, localvars]
+(*s A light version of [mind_specif_of_mind] with pre-splitted args
+   Invariant: We have \par
+   [Hnf (fullmind)] = [DOPN(AppL,[|MutInd mind;..params..;..realargs..|])] \par
+   with [mind]  = [((sp,i),localvars)] for some [sp, i, localvars].
  *)
 type inductive_summary = {
   fullmind : constr;
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 3a8f8a47a5..82d71fd4cb 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -9,7 +9,7 @@ open Term
 
 (* Signatures of named variables. *)
 
-type 'a signature (* = identifier list * 'a list*)
+type 'a signature (* = [identifier list * 'a list] *)
 
 val nil_sign : 'a signature
 val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 972109d2f1..6672a3d4b0 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -15,7 +15,7 @@ val the_conv_x : env -> 'a evar_defs -> constr -> constr -> bool
 
 val the_conv_x_leq : env -> 'a evar_defs -> constr -> constr -> bool
 
-(* For debugging *)
+(*i For debugging *)
 val solve_pb : 
   env -> 'a evar_defs -> conv_pb * constr * constr -> bool
 
@@ -26,3 +26,4 @@ val evar_conv_x :
 val evar_eqappr_x : 
   env -> 'a evar_defs ->
     conv_pb -> constr * constr list -> constr * constr list -> bool
+(*i*)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f29f79c617..f4c39fdb3c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -11,7 +11,7 @@ open Reduction
 (*i*)
 
 (* This modules provides useful functions for unification algorithms.
- * Used in Trad and Progmach
+ * Used in Trad and Progmach.
  * This interface will have to be improved. *)
 
 val filter_unique : 'a list -> 'a list
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 036cd53f0b..3f9ec15552 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -1,12 +1,12 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Evd
 open Environ
-
-type metamap = (int * constr) list
+(*i*)
 
 (* This family of functions assumes its constr argument is known to be
    well-typable. It does not type-check, just recompute the type
@@ -14,6 +14,8 @@ type metamap = (int * constr) list
    either produces a wrong result or raise an anomaly. Use with care.
    It doesn't handle predicative universes too. *)
 
+type metamap = (int * constr) list
+
 val get_type_of : env -> 'a evar_map -> constr -> constr
 val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
 val get_sort_of : env -> 'a evar_map -> constr -> sorts
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 5e268c320f..6aa76f617f 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -11,7 +11,7 @@ open Evd
 open Environ
 (*i*)
 
-(* This module declares the structure of proof trees, global and
+(* This module declares the structures of proof trees, global and
    readable constraints, and a few utilities on these types *)
 
 type bindOcc = 
diff --git a/toplevel/doc.tex b/toplevel/doc.tex
index 845d5901d3..f2550fda11 100644
--- a/toplevel/doc.tex
+++ b/toplevel/doc.tex
@@ -7,4 +7,4 @@ This chapter describes the highest modules of the \Coq\ system.
 They are organized as follows:
 
 \bigskip
-\begin{center}\epsfig{file=pretyping.dep.ps,width=\linewidth}\end{center}
+\begin{center}\epsfig{file=toplevel.dep.ps,width=\linewidth}\end{center}