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

1 files changed, 221 insertions, 211 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 1a3f29c73..c484a68d5 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) *