mise en place programmation literaire (generation de doc/coq.tex)

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

8 files changed, 294 insertions, 255 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 52f2ad038c..fb7431e4e7 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -1,12 +1,14 @@
 
 (* $Id$ *)
 
+(*i*)
 open Pp
 open Names
 open Generic
 open Term
 open Evd
 open Environ
+(*i*)
 
 (* flags for profiling... *)
 val stats : bool ref
diff --git a/kernel/evd.mli b/kernel/evd.mli
index cb606941c0..8ed6babc08 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -1,36 +1,43 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
 open Sign
+(*i*)
 
-(* The type of mappings for existential variables *)
+(* The type of mappings for existential variables.
+   The keys are section paths and the associated information is a record
+   containing the type of the evar ([concl]), the signature under which 
+   it was introduced ([hyps]), its definition ([body]) and any other 
+   possible information if necessary ([info]).
+*)
 
 type evar_body =
   | EVAR_EMPTY 
   | EVAR_DEFINED of constr
 
 type 'a evar_info = {
-  concl : constr;            (* the type of the evar ...                 *)
-  hyps  : context;           (* ... under a certain signature            *)
-  body  : evar_body;         (* its definition                           *) 
-  info  : 'a option          (* any other possible information necessary *)
-}         
+  concl : constr;
+  hyps  : context;
+  body  : evar_body;
+  info  : 'a option }
 
 type 'a evar_map
 
-val dom    : 'c evar_map -> section_path list
-val map    : 'c evar_map -> section_path -> 'c evar_info
-val rmv    : 'c evar_map -> section_path -> 'c evar_map
-val remap  : 'c evar_map -> section_path -> 'c evar_info -> 'c evar_map
-val in_dom : 'c evar_map -> section_path -> bool
-val toList : 'c evar_map -> (section_path * 'c evar_info) list
+val dom    : 'a evar_map -> section_path list
+val map    : 'a evar_map -> section_path -> 'a evar_info
+val rmv    : 'a evar_map -> section_path -> 'a evar_map
+val remap  : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
+val in_dom : 'a evar_map -> section_path -> bool
+val toList : 'a evar_map -> (section_path * 'a evar_info) list
 
-val mt_evd : 'c evar_map
+val mt_evd : 'a evar_map
 val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
-val add_noinfo : 'a evar_map -> section_path -> context -> 
-                 constr -> 'a evar_map
+val add_noinfo : 
+  'a evar_map -> section_path -> context -> constr -> 'a evar_map
+
 val define : 'a evar_map -> section_path -> constr -> 'a evar_map
 
 val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
diff --git a/kernel/generic.mli b/kernel/generic.mli
index c9d3dd73df..20b24c68a9 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -1,12 +1,17 @@
 
 (* $Id$ *)
 
+(*i*)
 open Util
 open Names
+(*i*)
 
 exception FreeVar
 exception Occur
 
+(* \label{generic_terms}
+   Generic terms, over any kind of operators. *)
+
 type 'oper term =
   | DOP0 of 'oper                            (* atomic terms *)
   | DOP1 of 'oper * 'oper term               (* operator of arity 1 *)
@@ -42,9 +47,9 @@ val reloc_rel: int -> lift_spec -> int
 type 'a subs =
   | ESID                   (* ESID       =          identity *)
   | CONS of 'a * 'a subs   (* CONS(t,S)  = (S.t)    parallel substitution *)
-  | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
+  | SHIFT of int * 'a subs (* SHIFT(n,S)= (\^n o S) terms in S are relocated *)
                            (*                        with n vars *)
-  | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
+  | LIFT of int * 'a subs  (* LIFT(n,S)=(\%n S) stands for ((\^n o S).n...1) *)
 
 val subs_cons  : 'a * 'a subs -> 'a subs
 val subs_lift  : 'a subs -> 'a subs
diff --git a/kernel/names.mli b/kernel/names.mli
index 0ca83f70d6..6968d7b967 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -1,7 +1,9 @@
 
 (* $Id$ *)
 
+(*i*)
 open Pp
+(*i*)
 
 type identifier
 type name = Name of identifier | Anonymous
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 058db0a117..46ffc42a18 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Generic
 open Term
@@ -8,33 +9,33 @@ open Univ
 open Environ
 open Closure
 open Evd
+(*i*)
+
+(* Reduction Functions. *)
 
 exception Redelimination
 exception Induc
 exception Elimconst
 
 type 'a reduction_function = 'a unsafe_env -> constr -> constr
-type 'a stack_reduction_function = 'a unsafe_env -> constr -> constr list 
-  -> constr * constr list
+
+type 'a stack_reduction_function = 
+    'a unsafe_env -> constr -> constr list -> constr * constr list
 
 val whd_stack : 'a stack_reduction_function
 
-(* Reduction Function Operators *)
-val under_casts      : 'a reduction_function -> 'a reduction_function
-val strong           : 'a reduction_function -> 'a reduction_function
+(*s Reduction Function Operators *)
+val under_casts : 'a reduction_function -> 'a reduction_function
+val strong : 'a reduction_function -> 'a reduction_function
 val strong_prodspine : 'a reduction_function -> 'a reduction_function
 val stack_reduction_of_reduction : 
   'a reduction_function -> 'a stack_reduction_function
 
-(*************************
- ** Reduction Functions **
- *************************)
-
-(* Generic Optimized Reduction Functions using Closures *)
+(*s Generic Optimized Reduction Functions using Closures *)
 
 (* 1. lazy strategy *)
 val clos_norm_flags : Closure.flags -> 'a reduction_function
-(* Same as (strong whd_beta[delta][iota]), but much faster on big terms *) 
+(* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
 val nf_beta : 'a reduction_function
 val nf_betaiota : 'a reduction_function
 val nf_betadeltaiota : 'a reduction_function
@@ -55,7 +56,7 @@ val whd_betaiota_stack : 'a stack_reduction_function
 val whd_betadeltaiota_stack : 'a stack_reduction_function
 
 
-(* Head normal forms *)
+(*s Head normal forms *)
 val whd_const_stack : section_path list -> 'a stack_reduction_function
 val whd_const : section_path list -> 'a reduction_function
 val whd_delta_stack : 'a stack_reduction_function
@@ -72,7 +73,7 @@ val whd_betadeltaiotaeta : 'a reduction_function
 val beta_applist : (constr * constr list) -> constr
 
 
-(* Special-Purpose Reduction Functions *)
+(*s Special-Purpose Reduction Functions *)
 val whd_meta : 'a reduction_function
 val plain_instance : 'a reduction_function
 val instance : 'a reduction_function
@@ -88,10 +89,14 @@ val one_step_reduce : 'a reduction_function
 val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
   'c unsafe_env -> string -> constr -> constr array -> constr
-val hnf_prod_applist : 'c unsafe_env -> string -> constr -> constr list -> constr
-val hnf_lam_app : 'c unsafe_env -> string -> constr -> constr -> constr
-val hnf_lam_appvect : 'c unsafe_env -> string -> constr -> constr array -> constr
-val hnf_lam_applist : 'c unsafe_env -> string -> constr -> constr list -> constr
+val hnf_prod_applist : 
+  'c unsafe_env -> string -> constr -> constr list -> constr
+val hnf_lam_app : 
+  'c unsafe_env -> string -> constr -> constr -> constr
+val hnf_lam_appvect : 
+  'c unsafe_env -> string -> constr -> constr array -> constr
+val hnf_lam_applist : 
+  'c unsafe_env -> string -> constr -> constr list -> constr
 val splay_prod : 'c unsafe_env -> constr -> (name * constr) list * constr
 val decomp_prod : 'c unsafe_env -> constr -> int * constr
 val decomp_n_prod : 
@@ -110,7 +115,8 @@ val reduce_to_ind  : 'c unsafe_env -> constr ->
 
 val whd_programs : 'a reduction_function
 
-(* Generic reduction: reduction functions associated to tactics *)
+
+(*s Generic reduction: reduction functions associated to tactics *)
 type red_expr =
   | Red
   | Hnf
@@ -134,7 +140,7 @@ val compute : 'a reduction_function
 val reduction_of_redexp : red_expr -> 'a reduction_function
 
 
-(* Conversion Functions (uses closures, lazy strategy) *)
+(*s Conversion Functions (uses closures, lazy strategy) *)
 
 type conversion_result =
   | Convertible of universes
@@ -146,20 +152,24 @@ type 'a conversion_function =
 val sort_cmp : conv_pb -> sorts -> sorts -> universes -> conversion_result
 
 val fconv : conv_pb -> 'a conversion_function
+
 (* fconv has 4 instances:
- * conv   = fconv CONV   : conversion test, and adjust universes constraints
- * conv_x = fconv CONV_X :     id.        , without adjusting univ 
+   \begin{itemize}
+   \item [conv = fconv CONV] : 
+     conversion test, and adjust universes constraints
+   \item [conv_x = fconv CONV_X] : idem, without adjusting univ 
      (used in tactics)
- * conv_leq   = fconv CONV_LEQ   : cumulativity test, adjust universes
- * conv_x_leq = fconv CONV_X_LEQ :       id.        , without adjusting 
-     (in tactics)
- *)
+   \item [conv_leq = fconv CONV_LEQ] : cumulativity test, adjust universes
+   \item [conv_x_leq = fconv CONV_X_LEQ] : idem, without adjusting 
+     (used in tactics)
+   \end{itemize} *)
 val conv : 'a conversion_function
 val conv_leq : 'a conversion_function
 val conv_x : 'a conversion_function
 val conv_x_leq : 'a conversion_function
 
-(* Obsolete Reduction Functions *)
+
+(*s Obsolete Reduction Functions *)
 
 val hnf : 'a unsafe_env -> constr -> constr * constr list
 val apprec : 'a stack_reduction_function
@@ -171,5 +181,5 @@ val check_mrectype_spec : 'a unsafe_env -> constr -> constr
 val minductype_spec : 'a unsafe_env -> constr -> constr
 val mrectype_spec : 'a unsafe_env -> constr -> constr
 
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
+(* Special function, which keep the key casts under Fix and MutCase. *)
 val strip_all_casts : constr -> constr
diff --git a/kernel/sign.mli b/kernel/sign.mli
index b07fcd0310..d2c271a7dd 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -1,9 +1,11 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Generic
 open Term
+(*i*)
 
 type 'a signature = identifier list * 'a list
 type 'a db_signature = (name * 'a) list
diff --git a/kernel/term.ml b/kernel/term.ml
index bdf4613408..7d3b9f7ff4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -687,6 +687,7 @@ let nb_prod =
   in 
   nbrec 0
 
+
 (********************************************************************)
 (*   various utility functions for implementing terms with bindings *)
 (********************************************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 1a3f29c732..c484a68d5c 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -1,12 +1,13 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Generic
+(*i*)
 
-(* The Type of Constructions Terms. *)
-
-(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
+(*s The operators of the Calculus of Inductive Constructions. 
+  ['a] is the type of sorts. *)
 
 type 'a oper = 
   (* DOP0 *)
@@ -29,6 +30,8 @@ type 'a oper =
 
 and case_info = (section_path * int) option
 
+(*s The sorts of CCI. *)
+
 type contents = Pos | Null
 
 val str_of_contents : contents -> string
@@ -41,6 +44,11 @@ type sorts =
 val mk_Set  : sorts
 val mk_Prop : sorts
 
+(*s The type [constr] of the terms of CCI
+  is obtained by instanciating the generic terms (type [term], 
+  see \ref{generic_terms}) on the above operators, themselves instanciated
+  on the above sorts. *)
+
 type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
@@ -51,15 +59,12 @@ type term_judgment = type_judgment judge
 type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
 
 
-(****************************************************************************)
-(*              Functions for dealing with constr terms                     *)
-(****************************************************************************)
-
-(* The following functions are intended to simplify and to uniform the 
-   manipulation of terms. Some of these functions may be overlapped with
-   previous ones. *)
+(*s Functions for dealing with constr terms.
+  The following functions are intended to simplify and to uniform the 
+  manipulation of terms. Some of these functions may be overlapped with
+  previous ones. *)
 
-(* Concrete type for making pattern-matching *)
+(*  Concrete type for making pattern-matching. *)
 
 type kindOfTerm =
   | IsRel          of int
@@ -82,79 +87,78 @@ type kindOfTerm =
   | IsCoFix        of int * constr array * name list * constr array
 
 (* Discriminates which kind of term is it.  
-   Note that there is no cases for [[DLAM] and [DLAMV].  These terms do not
-   make sense alone, but they must be preceeded by the application of
-   an operator.  
-*)
+  Note that there is no cases for [DLAM] and [DLAMV].  These terms do not
+  make sense alone, but they must be preceeded by the application of
+  an operator. *)
 
 val kind_of_term : constr -> kindOfTerm
 
-(*********************)
-(* Term constructors *)
-(*********************)
+
+(*s Term constructors. *)
 
 (* Constructs a DeBrujin index *)
-val mkRel          : int -> constr
+val mkRel : int -> constr
 
 (* Constructs an existential variable named "?" *)
-val mkExistential  : constr
+val mkExistential : constr
 
 (* Constructs an existential variable named "?n" *)
-val mkMeta         : int -> constr
+val mkMeta : int -> constr
 
 (* Constructs a Variable *)
-val mkVar          : identifier -> constr
+val mkVar : identifier -> constr
 
-(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
-val mkXtra         : string -> Coqast.t list -> constr
+(* Construct an  [XTRA] term. *)
+val mkXtra : string -> Coqast.t list -> constr
 
 (* Construct a type *)
-val mkSort         : sorts -> constr
-val mkProp         : constr
-val mkSet          : constr 
-val mkType         : Univ.universe -> constr
+val mkSort : sorts -> constr
+val mkProp : constr
+val mkSet : constr 
+val mkType : Univ.universe -> constr
 val prop : sorts
 val spec : sorts
 val types : sorts 
 val type_0 : sorts
 val type_1 : sorts
 
-(* Construct an implicit (see implicit arguments in the RefMan) *)
-(* Used for extraction *)
-val mkImplicit     : constr
-val implicit_sort  : sorts
+(* Construct an implicit (see implicit arguments in the RefMan).
+   Used for extraction *)
+val mkImplicit : constr
+val implicit_sort : sorts
 
-(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
-(* (that means t2 is declared as the type of t1) *)
-val mkCast         : constr -> constr -> constr
+(* Constructs the term $t_1::t2$, i.e. the term $t_1$ casted with the 
+   type $t_2$ (that means t2 is declared as the type of t1). *)
+val mkCast : constr -> constr -> constr
 
-(* Constructs the product (x:t1)t2  -- x may be anonymous *)
-val mkProd         : name -> constr -> constr -> constr
+(* Constructs the product $(x:t_1)t_2$. $x$ may be anonymous. *)
+val mkProd : name -> constr -> constr -> constr
 
-(* non-dependant product t1 -> t2 *)
+(* non-dependant product $t_1 \rightarrow t_2$ *)
 val mkArrow : constr -> constr -> constr
 
 (* named product *)
 val mkNamedProd : identifier -> constr -> constr -> constr
 
-(* Constructs the abstraction [x:t1]t2 *)
-val mkLambda       : name -> constr -> constr -> constr
+(* Constructs the abstraction $[x:t_1]t_2$ *)
+val mkLambda : name -> constr -> constr -> constr
 val mkNamedLambda : identifier -> constr -> constr -> constr
 
-(* If a = [| t1; ...; tn |], constructs the application (t1 ... tn) *)
-val mkAppL         : constr array -> constr
-val mkAppList      : constr list  -> constr
+(* If $a = [| t_1; \dots; t_n |]$, constructs the application 
+   $(t_1~\dots~t_n)$. *)
+val mkAppL : constr array -> constr
+val mkAppList : constr list  -> constr
 
 (* Constructs a constant *) 
 (* The array of terms correspond to the variables introduced in the section *)
-val mkConst        : section_path -> constr array -> constr
+val mkConst : section_path -> constr array -> constr
 
 (* Constructs an abstract object *)
-val mkAbst         : section_path -> constr array -> constr
+val mkAbst : section_path -> constr array -> constr
 
 (* Constructs the ith (co)inductive type of the block named sp *)
 (* The array of terms correspond to the variables introduced in the section *)
-val mkMutInd       : section_path -> int -> constr array -> constr
+val mkMutInd : section_path -> int -> constr array -> constr
 
 (* Constructs the jth constructor of the ith (co)inductive type of the 
    block named sp. The array of terms correspond to the variables
@@ -162,157 +166,156 @@ val mkMutInd       : section_path -> int -> constr array -> constr
 val mkMutConstruct : section_path -> int -> int -> constr array -> constr
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-val mkMutCase      : case_info -> constr -> constr -> constr list -> constr
-val mkMutCaseA     : case_info -> constr -> constr -> constr array -> constr
+val mkMutCase : case_info -> constr -> constr -> constr list -> constr
+val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
 
-(* If recindxs = [|i1,...in|] 
-      typarray = [|t1,...tn|]
-      funnames = [f1,.....fn]
-      bodies   = [b1,.....bn]
-   then    
+(* If [recindxs = [|i1,...in|]]
+      [typarray = [|t1,...tn|]]
+      [funnames = [f1,.....fn]]
+      [bodies   = [b1,.....bn]]
+   then 
 
-      mkFix recindxs i typarray funnames bodies
+   [ mkFix recindxs i typarray funnames bodies]
    
-   constructs the ith function of the block  
+   constructs the $i$th function of the block  
 
-    Fixpoint f1 [ctx1] = b1
-    with     f2 [ctx2] = b2
-    ...
-    with     fn [ctxn] = bn.
+    [Fixpoint f1 [ctx1] = b1
+     with     f2 [ctx2] = b2
+     ...
+     with     fn [ctxn] = bn.]
 
-   where the lenght of the jth context is ij.
+   where the lenght of the $j$th context is $ij$.
 *)
-val mkFix          : int array -> int -> type_judgment array -> name list 
-                      -> constr array -> constr
+val mkFix : int array -> int -> type_judgment array -> name list 
+  -> constr array -> constr
 
 (* Similarly, but we assume the body already constructed *)
-val mkFixDlam      : int array -> int -> type_judgment array
-                     -> constr array -> constr 
+val mkFixDlam : int array -> int -> type_judgment array
+  -> constr array -> constr 
 
-(* If typarray = [|t1,...tn|]
-      funnames = [f1,.....fn]
-      bodies   = [b1,.....bn]
+(* If [typarray = [|t1,...tn|]]
+      [funnames = [f1,.....fn]]
+      [bodies   = [b1,.....bn]]
    then
 
-      mkCoFix i typsarray funnames bodies 
+      [mkCoFix i typsarray funnames bodies]
 
    constructs the ith function of the block  
    
-    CoFixpoint f1 = b1
-    with       f2 = b2
-    ...
-    with       fn = bn.
-
-*)
-val mkCoFix        : int -> type_judgment array -> name list 
-                     -> constr array -> constr
+    [CoFixpoint f1 = b1
+     with       f2 = b2
+     ...
+     with       fn = bn.]
+ *)
+val mkCoFix : int -> type_judgment array -> name list 
+  -> constr array -> constr
 
 (* Similarly, but we assume the body already constructed *)
-val mkCoFixDlam    : int -> type_judgment array -> constr array -> constr
+val mkCoFixDlam : int -> type_judgment array -> constr array -> constr
 
-(********************)
-(* Term destructors *)
-(********************)
 
-(* Destructor operations : partial functions 
-   Raise invalid_arg "dest*" if the const has not the expected form *)
+(*s Term destructors. 
+   Destructor operations are partial functions and
+   raise [invalid_arg "dest*"] if the term has not the expected form. *)
 
 (* Destructs a DeBrujin index *)
-val destRel          : constr -> int
+val destRel : constr -> int
 
 (* Destructs an existential variable *)
-val destMeta         : constr -> int
+val destMeta : constr -> int
 val isMETA : constr -> bool
 
 (* Destructs a variable *)
-val destVar          : constr -> identifier
+val destVar : constr -> identifier
 
 (* Destructs an XTRA *)
-val destXtra        : constr -> string * Coqast.t list
+val destXtra : constr -> string * Coqast.t list
 
-(* Destructs a sort *)
-val destSort         : constr -> sorts
+(* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether 
+   [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *)
+val destSort : constr -> sorts
 val contents_of_kind : constr -> contents
-val is_Prop          : constr -> bool (* true for Prop *) 
-val is_Set           : constr -> bool  (* true for Set *)
-val isprop           : constr -> bool (* true for DOP0 (Sort (Prop _)) *)
-val is_Type          : constr -> bool (* true for DOP0 (Sort (Type _)) *)
-val iskind           : constr -> bool (* true for Prop, Set and Type(_) *)
+val is_Prop : constr -> bool
+val is_Set : constr -> bool
+val isprop : constr -> bool
+val is_Type : constr -> bool
+val iskind : constr -> bool
 
-val isType           : sorts -> bool (* true for Type(_) *)
-val is_small         : sorts -> bool (* true for Prop and Set *)
+val isType : sorts -> bool
+val is_small : sorts -> bool (* true for \textsf{Prop} and \textsf{Set} *)
 
 (* Destructs a casted term *)
-val destCast         : constr -> constr * constr
+val destCast : constr -> constr * constr
 val cast_type : constr -> constr (* 2nd proj *)
 val cast_term : constr -> constr (* 1st proj *)
 val isCast : constr -> bool
-(* removes recursively the casts around a term *)
-(* strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c *)
+
+(* Removes recursively the casts around a term i.e.
+   [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
 val strip_outer_cast : constr -> constr
 
-(* Destructs the product (x:t1)t2 *)
-val destProd          : constr -> name * constr * constr
-val hd_of_prod        : constr -> constr
+(* Destructs the product $(x:t_1)t_2$ *)
+val destProd : constr -> name * constr * constr
+val hd_of_prod : constr -> constr
 val hd_is_constructor : constr -> bool
 
-(* Destructs the abstraction [x:t1]t2 *)
-val destLambda       : constr -> name * constr * constr
+(* Destructs the abstraction $[x:t_1]t_2$ *)
+val destLambda : constr -> name * constr * constr
 
 (* Destructs an application *)
-val destAppL   : constr -> constr array
-val isAppL     : constr -> bool
-val hd_app     : constr -> constr 
-val args_app   : constr -> constr array
+val destAppL : constr -> constr array
+val isAppL : constr -> bool
+val hd_app : constr -> constr 
+val args_app : constr -> constr array
 
 (* Destructs a constant *)
-val destConst     : constr -> section_path * constr array
+val destConst : constr -> section_path * constr array
 val path_of_const : constr -> section_path
 val args_of_const : constr -> constr array
 
 (* Destrucy an abstract term *)
-val destAbst         : constr -> section_path * constr array
+val destAbst : constr -> section_path * constr array
 val path_of_abst : constr -> section_path
 val args_of_abst : constr -> constr array
 
 (* Destructs a (co)inductive type *)
-val destMutInd    : constr -> section_path * int * constr array
-val op_of_mind    : constr -> section_path * int
-val args_of_mind  : constr -> constr array
-val ci_of_mind    : constr -> case_info
+val destMutInd : constr -> section_path * int * constr array
+val op_of_mind : constr -> section_path * int
+val args_of_mind : constr -> constr array
+val ci_of_mind : constr -> case_info
 
 (* Destructs a constructor *)
 val destMutConstruct : constr -> section_path * int * int * constr array
-val op_of_mconstr    : constr -> (section_path * int) * int
-val args_of_mconstr  : constr -> constr array
+val op_of_mconstr : constr -> (section_path * int) * int
+val args_of_mconstr : constr -> constr array
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
-val destCase         : constr -> case_info * constr * constr * constr array
+val destCase : constr -> case_info * constr * constr * constr array
 
 (* Destructs the ith function of the block  
-    Fixpoint f1 [ctx1] = b1
-    with     f2 [ctx2] = b2
-    ...
-    with     fn [ctxn] = bn.
+    [Fixpoint f1 [ctx1] = b1
+     with     f2 [ctx2] = b2
+     ...
+     with     fn [ctxn] = bn.]
 
-   where the lenght of the jth context is ij.
+   where the lenght of the $j$th context is $ij$.
 *)
-val destGralFix      : constr array -> constr array * Names.name list 
-                                        * constr array
-val destFix          : constr -> int array * int * type_judgment array
-                                  * Names.name list * constr array
-val destCoFix        : constr -> int * type_judgment array * Names.name list 
-                                  * constr array
+val destGralFix : 
+  constr array -> constr array * Names.name list * constr array
+val destFix : constr -> 
+  int array * int * type_judgment array * Names.name list * constr array
+
+val destCoFix : 
+  constr -> int * type_judgment array * Names.name list * constr array
 
 (* Provisoire, le temps de maitriser les cast *)
-val destUntypedFix          : constr -> int array * int * constr array
-                                  * Names.name list * constr array
-val destUntypedCoFix        : constr -> int * constr array * Names.name list 
-                                  * constr array
+val destUntypedFix : 
+  constr -> int array * int * constr array * Names.name list * constr array
+val destUntypedCoFix : 
+  constr -> int * constr array * Names.name list * constr array
+
 
-(***********************************)
-(* Other term constructors         *)
-(***********************************)
+(*s Other term constructors. *)
 
 val abs_implicit : constr -> constr
 val lambda_implicit : constr -> constr
@@ -322,127 +325,136 @@ val applist : constr * constr list -> constr
 val applistc : constr -> constr list -> constr
 val appvect : constr * constr array -> constr
 val appvectc : constr -> constr array -> constr
-(* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *)
-val prodn   : int -> (name * constr) list -> constr -> constr
-(* lamn n ([x1:T1]..[xn:T]Gamma) b = [x1:T1]..[xn:Tn]b *)
+
+(* [prodn n l b] = $(x_1:T_1)..(x_n:T_n)b$ 
+   where $l = [(x_1,T_1);\dots;(x_n,T_n);Gamma]$ *)
+val prodn : int -> (name * constr) list -> constr -> constr
+
+(* [lamn n l b] = $[x_1:T_1]..[x_n:T_n]b$
+   where $l = [(x_1,T_1);\dots;(x_n,T_n);Gamma]$ *)
 val lamn : int -> (name * constr) list -> constr -> constr
 
-(* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *)
+(* [prod_it b l] = $(x_1:T_1)..(x_n:T_n)b$ 
+   where $l = [x_1:T_1;..x_n:T_n]$ *)
 val prod_it : constr -> (name * constr) list -> constr
-(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *)
-val lam_it : constr -> (name * constr) list -> constr
 
+(* [lam_it b l] = $[x_1:T_1]..[x_n:T_n]b$ 
+   where $l = [x_1:T_1;..;x_n:T_n]$ *)
+val lam_it : constr -> (name * constr) list -> constr
 
-(* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T =
-   [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *)
+(* [to_lambda n l] 
+   = $[x_1:T_1]...[x_n:T_n](x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$
+   where $l = (x_1:T_1)...(x_n:T_n)(x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ *)
 val to_lambda : int -> constr -> constr
 val to_prod : int -> constr -> constr
 
-(*********************************)
-(* Other term destructors        *)
-(*********************************)
 
-(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
-   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
-val decompose_prod  : constr -> (name*constr) list * constr
+(*s Other term destructors. *)
+
+(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
+   $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. *)
+val decompose_prod : constr -> (name*constr) list * constr
 
-(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
-   ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
-val decompose_lam   : constr -> (name*constr) list * constr
+(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair
+   $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a lambda. *)
+val decompose_lam : constr -> (name*constr) list * constr
 
-(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
-   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
-val decompose_prod_n  : int -> constr -> (name*constr) list * constr
+(* Given a positive integer n, transforms a product term 
+   $(x_1:T_1)..(x_n:T_n)T$
+   into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
+val decompose_prod_n : int -> constr -> (name*constr) list * constr
 
-(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
-   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
-val decompose_lam_n   : int -> constr -> (name*constr) list * constr
+(* Given a positive integer $n$, transforms a lambda term 
+   $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
+val decompose_lam_n : int -> constr -> (name*constr) list * constr
 
-(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
- * gives n (casts are ignored) *)
+(* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction
+   gives $n$ (casts are ignored) *)
 val nb_lam : constr -> int
 
-(* similar to nb_lam, but gives the number of products instead *)
+(* similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
-(********************************************************************)
-(*   various utility functions for implementing terms with bindings *)
-(********************************************************************)
+
+(*s Various utility functions for implementing terms with bindings. *)
 
 val extract_lifted : int * constr -> constr
 val insert_lifted : constr -> int * constr
 
-(* l is a list of pairs (n:nat,x:constr), env is a stack of (na:name,T:constr)
-   push_and_lift adds a component to env and lifts l one step *)
+(* If [l] is a list of pairs $(n:nat,x:constr)$, [env] is a stack of 
+   $(na:name,T:constr)$, then
+   [push_and_lift (id,c) env l] adds a component [(id,c)] to [env] 
+   and lifts [l] one step *)
 val push_and_lift :
   name * constr -> (name * constr) list -> (int * constr) list 
     -> (name * constr) list * (int * constr) list
 
-(* if T is not (x1:A1)(x2:A2)....(xn:An)T' then (push_and_liftl n env T l)
-   raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')
-   where l' is l lifted n steps *)
+(* if [T] is not $(x_1:A_1)(x_2:A_2)....(x_n:A_n)T'$ 
+   then [(push_and_liftl n env T l)]
+   raises an error else it gives $([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')$
+   where $l'$ is [l] lifted [n] steps *)
 val push_and_liftl :
   int -> (name * constr) list -> constr -> (int * constr) list
     -> (name * constr) list * constr * (int * constr) list
 
-(* if T is not [x1:A1][x2:A2]....[xn:An]T' then (push_lam_and_liftl n env T l)
-   raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l')
-   where l' is l lifted n steps *)
+(* if $T$ is not $[x_1:A_1][x_2:A_2]....[x_n:A_n]T'$ then 
+   [(push_lam_and_liftl n env T l)]
+   raises an error else it gives $([x_1,A_1; x_2,A_2; ...; x_n,A_n]@env,T',l')$
+   where $l'$ is [l] lifted [n] steps *)
 val push_lam_and_liftl :
   int -> (name * constr) list -> constr -> (int * constr) list
     -> (name * constr) list * constr * (int * constr) list
 
-(* l is a list of pairs (n:nat,x:constr), tlenv is a stack of
-(na:name,T:constr), B : constr, na : name
-(prod_and_pop ((na,T)::tlenv) B l) gives (tlenv, (na:T)B, l')
-where l' is l lifted down one step *)
+(* If [l] is a list of pairs $(n:nat,x:constr)$, [tlenv] is a stack of
+   $(na:name,T:constr)$, [B] is a constr, [na] a name, then
+   [(prod_and_pop ((na,T)::tlenv) B l)] gives $(tlenv, (na:T)B, l')$
+   where $l'$ is [l] lifted down one step *)
 val prod_and_pop :
   (name * constr) list -> constr -> (int * constr) list
     -> (name * constr) list * constr * (int * constr) list
 
-(* recusively applies prod_and_pop :
-if env = [na1:T1 ; na2:T2 ; ... ; nan:Tn]@tlenv
-then
-(prod_and_popl n env T l) gives (tlenv,(nan:Tn)...(na1:Ta1)T,l') where
-l' is l lifted down n steps *)
+(* recusively applies [prod_and_pop] :
+   if [env] = $[na_1:T_1 ; na_2:T_2 ; ... ; na_n:T_n]@tlenv$
+   then
+   [(prod_and_popl n env T l)] gives $(tlenv,(na_n:T_n)...(na_1:T_1)T,l')$
+   where $l'$ is [l] lifted down [n] steps *)
 val prod_and_popl :
   int -> (name * constr) list -> constr -> (int * constr) list
     -> (name * constr) list * constr * (int * constr) list
 
-(* similar to prod_and_pop, but gives [na:T]B intead of (na:T)B *)
+(* similar to [prod_and_pop], but gives $[na:T]B$ intead of $(na:T)B$ *)
 val lam_and_pop :
   (name * constr) list -> constr -> (int * constr) list
     -> (name * constr) list * constr * (int * constr) list
 
-(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
- * (nan:Tan)...(na1:Ta1)B *)
+(* similar to [prod_and_popl] but gives $[na_n:T_n]...[na_1:T_1]B$ instead of
+   $(na_n:T_n)...(na_1:T_1)B$ *)
 val lam_and_popl :
   int -> (name * constr) list -> constr -> (int * constr) list
     -> (name * constr) list * constr * (int * constr) list
 
-(* similar to lamn_and_pop but generates new names whenever the name is 
- * Anonymous *)
+(* similar to [lamn_and_pop] but generates new names whenever the name is 
+   [Anonymous] *)
 val lam_and_pop_named :
   (name * constr) list -> constr ->(int * constr) list ->identifier list 
     -> (name * constr) list * constr * (int * constr) list * identifier list
 
-(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
- * but it generates names whenever nai=Anonymous *)
+(* similar to [prod_and_popl] but gives $[na_n:T_n]...[na_1:T_1]B$ instead of
+   but it generates names whenever $na_i$ = [Anonymous] *)
 val lam_and_popl_named :
- int ->  (name * constr) list -> constr ->  (int * constr) list 
-  -> (name * constr) list * constr * (int * constr) list 
+  int ->  (name * constr) list -> constr ->  (int * constr) list 
+    -> (name * constr) list * constr * (int * constr) list 
+
 (* [lambda_ize n T endpt]
- * will pop off the first n products in T, then stick in endpt,
- * properly lifted, and then push back the products, but as lambda-
- * abstractions
- *)
-val lambda_ize :int ->'a oper term -> 'a oper term -> 'a oper term
+   will pop off the first [n] products in [T], then stick in [endpt],
+   properly lifted, and then push back the products, but as lambda-
+   abstractions *)
+val lambda_ize : int ->'a oper term -> 'a oper term -> 'a oper term
 
-(******************************************************************)
-(* Flattening and unflattening of embedded applications and casts *)
-(******************************************************************)
 
-(* if c is not an AppL, it is transformed into mkAppL [| c |] *)
+(*s Flattening and unflattening of embedded applications and casts. *)
+
+(* if [c] is not an [AppL], it is transformed into [mkAppL [| c |]] *)
 val ensure_appl : constr -> constr
 
 (* unflattens application lists *)
@@ -452,9 +464,7 @@ val collapse_appl : constr -> constr
 val decomp_app : constr -> constr * constr list
 
 
-(********************************************)
-(* Misc functions on terms, judgments, etc  *)
-(********************************************)
+(*s Misc functions on terms, sorts and conversion problems. *)
 
 (* Level comparison for information extraction : Prop <= Type *)
 val same_kind : constr -> constr -> bool
@@ -467,14 +477,13 @@ val pb_equal : conv_pb -> conv_pb
 val sort_hdchar : sorts -> string
 
 
-(***************************)
-(* occurs check functions  *)                         
-(***************************)
+(*s Occur check functions. *)                         
+
 val occur_meta : constr -> bool
 val rel_vect : int -> int -> constr array
 
-(* (occur_const (s:section_path) c) -> true if constant s occurs in c,
- * false otherwise *)
+(* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs 
+   in c, [false] otherwise *)
 val occur_const : section_path -> constr -> bool
 
 (* strips head casts and flattens head applications *)
@@ -492,10 +501,10 @@ val subst_term_eta_eq : constr -> constr -> constr
 val replace_consts :
   (section_path * (identifier list * constr) option) list -> constr -> constr
 
-(* bl : (int,constr) Listmap.t = (int * constr) list *)
-(* c : constr *)
-(* for each binding (i,c_i) in bl, substitutes the metavar i by c_i in c *)
-(* Raises Not_found if c contains a meta that is not in the association list *)
+(* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] 
+   for each binding $(i,c_i)$ in [bl],
+   and raises [Not_found] if [c] contains a meta that is not in the 
+   association list *) 
 
 val subst_meta : (int * constr) list -> constr -> constr
 
@@ -503,7 +512,8 @@ val subst_meta : (int * constr) list -> constr -> constr
 val matchable : constr -> constr
 val unmatchable: constr -> constr
 
-(* New hash-cons functions *)
+
+(*s Hash-consing functions for constr. *)
 
 val hcons_constr:
   (section_path -> section_path) *