Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

53 files changed, 258 insertions, 227 deletions

diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
index 04e38656..0a61ad79 100644
--- a/kernel/byterun/int64_emul.h
+++ b/kernel/byterun/int64_emul.h
@@ -11,7 +11,7 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id$ */
+/* $Id: int64_emul.h 10739 2008-04-01 14:45:20Z herbelin $ */
 
 /* Software emulation of 64-bit integer arithmetic, for C compilers
    that do not support it.  */
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
index f5bef4a6..4fc3c220 100644
--- a/kernel/byterun/int64_native.h
+++ b/kernel/byterun/int64_native.h
@@ -11,7 +11,7 @@
 /*                                                                     */
 /***********************************************************************/
 
-/* $Id$ */
+/* $Id: int64_native.h 10739 2008-04-01 14:45:20Z herbelin $ */
 
 /* Wrapper macros around native 64-bit integer arithmetic,
    so that it has the same interface as the software emulation
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index e7859962..0578c7b4 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -7,49 +7,46 @@ open Declarations
 open Pre_env
 
 
-(* Compilation des variables + calcul des variables libres               *)
+(* Compilation of variables + computing free variables                    *)
 
-(* Dans la machine virtuel il n'y a pas de difference entre les           *)
-(* fonctions et leur environnement                                        *)
+(* The virtual machine doesn't distinguish closures and their environment *)
 
-(* Representation de l'environnements des fonctions :                     *)
+(* Representation of function environments :                              *)
 (*        [clos_t | code | fv1 | fv2 | ... | fvn ]                        *)
 (*                ^                                                       *)
-(*  l'offset pour l'acces au variable libre est 1 (il faut passer le      *)
-(*  pointeur de code).                                                    *)
-(*  Lors de la compilation, les variables libres sont stock'ees dans      *)
-(*  [in_env] dans l'ordre inverse de la representation machine, ceci      *)
-(* permet de rajouter des nouvelles variables dans l'environnememt        *)
-(* facilement.                                                            *)
-(* Les arguments de la fonction arrive sur la pile dans l'ordre de        *)
-(* l'application :  f arg1 ... argn                                       *)
-(*   - la pile est alors :                                                *)
+(*  The offset for accessing free variables is 1 (we must skip the code   *)
+(*  pointer).                                                             *)
+(*  While compiling, free variables are stored in [in_env] in order       *)
+(*  opposite to machine representation, so we can add new free variables  *)
+(*  easily (i.e. without changing the position of previous variables)     *)
+(* Function arguments are on the stack in the same order as the           *)
+(* application :  f arg1 ... argn                                         *)
+(*   - the stack is then :                                                *)
 (*        arg1 : ... argn : extra args : return addr : ...                *)
-(* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn  *)
-(*  [n], [argn] par le de Bruijn [1]                                      *)
+(* In the function body [arg1] is represented by de Bruijn [n], and       *)
+(* [argn] by de Bruijn [1]                                                *)
 
-(* Representation des environnements des points fix mutuels :             *)
+(* Representation of environements of mutual fixpoints :                  *)
 (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
 (*                ^<----------offset--------->                            *)
 (* type = [Ct1 | .... | Ctn]                                              *)
-(* Ci est le code correspondant au corps du ieme point fix                *)
-(* Lors de l'evaluation d'un point fix l'environnement est un pointeur    *)
-(* sur la position correspondante a son code.                             *)
-(* Dans le corps de chaque point fix le de Bruijn [nbr] represente,       *)
-(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le       *)
-(* nbr-ieme.                                                              *)
-(* L'acces a ces variables se fait par l'instruction [Koffsetclosure]     *)
-(*  (decalage de l'environnement)                                         *)
-
-(* Ceci permet de representer tout les point fix mutuels en un seul bloc  *)
-(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des      *)
-(* types des points fixes, ils sont utilises pour tester la conversion    *)
-(* Leur environnement d'execution est celui du dernier point fix :        *)
+(* Ci is the code pointer of the i-th body                                *)
+(* At runtime, a fixpoint environment (which is the same as the fixpoint  *)
+(* itself) is a pointer to the field holding its code pointer.            *)
+(* In each fixpoint body, de Bruijn [nbr] represents the first fixpoint   *)
+(* and de Bruijn [1] the last one.                                        *)
+(* Access to these variables is performed by the [Koffsetclosure n]       *)
+(* instruction that shifts the environment pointer of [n] fields.         *)
+
+(* This allows to represent mutual fixpoints in just one block.           *)
+(* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint    *)
+(* types. They are used in conversion tests (which requires that          *)
+(* fixpoint types must be convertible). Their environment is the one of   *)
+(* the last fixpoint :                                                    *)
 (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
 (*                                ^                                       *)
 
-
-(* Representation des cofix mutuels :                                     *)
+(* Representation of mutual cofix :                                       *)
 (*  a1 =   [A_t | accumulate | [Cfx_t | fcofix1 ] ]                       *)
 (*                ...                                                     *)
 (*  anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ]                     *)
@@ -59,29 +56,28 @@ open Pre_env
 (*                ...                                                     *)
 (*  fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *)
 (*                      ^                                                 *)
-(*  Les block [ai] sont des fonctions qui accumulent leurs arguments :    *)
+(* The [ai] blocks are functions that accumulate their arguments:         *)
 (*           ai arg1  argp --->                                           *)
 (*    ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ]   *)
-(* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation,      *)
-(* la fonction [fcofixi] est alors appliqu'ee a [ai'] [arg1] ... [argp]   *)
-(* A la fin de l'evaluation [ai'] est mis a jour avec le resultat de      *)
-(* l'evaluation :                                                         *)
+(* If such a block is matched against, we have to force evaluation,       *)
+(* function [fcofixi] is then applied to [ai'] [arg1] ... [argp]          *)
+(* Once evaluation is completed [ai'] is updated with the result:         *)
 (*  ai' <--                                                               *)
 (*   [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ]   *)
-(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *)
-(* fois l'application d'un cofix (evaluation lazy)                        *)
-(* De plus elle permet de creer facilement des cycles quand les cofix ne  *)
-(* n'ont pas d'aruments, ex:                                              *)
+(* This representation is nice because the application of the cofix is    *)
+(* evaluated only once (it simulates a lazy evaluation)                   *)
+(* Moreover, when cofix don't have arguments, it is possible to create    *)
+(* a cycle, e.g.:                                                         *)
 (*   cofix one := cons 1 one                                              *)
 (*   a1 = [A_t | accumulate | [Cfx_t|fcofix1] ]                           *)
 (*   fcofix1 = [clos_t | code | a1]                                       *)
-(*  Quand on force l'evaluation de [a1] le resultat est                   *)
-(*    [cons_t | 1 | a1]                                                   *)
-(*  [a1] est mis a jour :                                                 *)
+(* The result of evaluating [a1] is [cons_t | 1 | a1].                    *)
+(* When [a1] is updated :                                                 *)
 (*  a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ]     *)
-(* Le cycle est cree ...                                                  *)
-
-(* On conserve la fct de cofix pour la conversion                         *)
+(* The cycle is created ...                                               *)
+(*                                                                        *)
+(* In Cfxe_t accumulators, we need to store [fcofixi] for testing         *)
+(* conversion of cofixpoints (which is intentional).                      *)
 
 
 let empty_fv = { size= 0;  fv_rev = [] }
@@ -112,7 +108,7 @@ let comp_env_fun arity =
   }
 
 
-let comp_env_type rfv =
+let comp_env_fix_type rfv =
   { nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
@@ -134,6 +130,15 @@ let comp_env_fix ndef curr_pos arity rfv =
      in_env = rfv
    }
 
+let comp_env_cofix_type ndef rfv =
+  { nb_stack = 0;
+    in_stack = [];
+    nb_rec = 0;
+    pos_rec = [];
+    offset = 1+ndef;
+    in_env = rfv
+  }
+
 let comp_env_cofix ndef arity rfv =
    let prec = ref [] in
    for i = 1 to ndef do
@@ -147,14 +152,13 @@ let comp_env_cofix ndef arity rfv =
      in_env = rfv
    }
 
-(* [push_param ] ajoute les parametres de fonction dans la pile *)
+(* [push_param ] add function parameters on the stack *)
 let push_param n sz r =
   { r with
     nb_stack = r.nb_stack + n;
     in_stack = add_param n sz r.in_stack }
 
-(* [push_local e sz] ajoute une nouvelle variable dans la pile a la *)
-(* position [sz]                                                    *)
+(* [push_local sz r] add a new variable on the stack at position [sz] *)
 let push_local sz r =
   { r with
     nb_stack = r.nb_stack + 1;
@@ -185,7 +189,7 @@ let pos_rel i r sz =
     let i = i - r.nb_stack in
     if i <= r.nb_rec then
       try List.nth r.pos_rec (i-1)
-      with _ -> assert false
+      with (Failure _|Invalid_argument _) -> assert false
     else
       let i = i - r.nb_rec in
       let db = FVrel(i) in
@@ -297,19 +301,19 @@ let cont_cofix arity =
     Kreturn (arity+2) ]
 
 
-(*i Global environment global *)
+(*i Global environment *)
 
 let global_env = ref empty_env
 
 let set_global_env env = global_env := env
 
 
-(* Code des fermetures *)
+(* Code of closures *)
 let fun_code = ref []
 
 let init_fun_code () = fun_code := []
 
-(* Compilation des constructeurs et des inductifs *)
+(* Compilation of constructors and inductive types *)
 
 (* Inv : nparam + arity > 0 *)
 let code_construct tag nparams arity cont =
@@ -424,7 +428,7 @@ let rec str_const c =
       end
   | _ -> Bconstr c
 
-(* compilation des applications *)
+(* compiling application *)
 let comp_args comp_expr reloc args sz cont =
   let nargs_m_1 = Array.length args - 1 in
   let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in
@@ -451,7 +455,7 @@ let comp_app comp_fun comp_arg reloc f args sz cont =
 	(comp_args comp_arg reloc args (sz + 3)
 	   (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1))))
 
-(* Compilation des variables libres *)
+(* Compiling free variables *)
 
 let compile_fv_elem reloc fv sz cont =
   match fv with
@@ -466,7 +470,7 @@ let rec compile_fv reloc l sz cont =
       compile_fv_elem reloc fvn sz
 	(Kpush :: compile_fv reloc tl (sz + 1) cont)
 
-(* compilation des constantes *)
+(* Compiling constants *)
 
 let rec get_allias env kn =
   let tps = (lookup_constant kn env).const_body_code in
@@ -475,7 +479,7 @@ let rec get_allias env kn =
   | _ -> kn
 
 
-(* compilation des expressions *)
+(* Compiling expressions *)
 
 let rec compile_constr reloc c sz cont =
   match kind_of_term c with
@@ -522,7 +526,7 @@ let rec compile_constr reloc c sz cont =
       let lbl_types = Array.create ndef Label.no in
       let lbl_bodies = Array.create ndef Label.no in
       (* Compilation des types *)
-      let env_type = comp_env_type rfv in
+      let env_type = comp_env_fix_type rfv in
       for i = 0 to ndef - 1 do
 	let lbl,fcode =
 	  label_code
@@ -530,7 +534,7 @@ let rec compile_constr reloc c sz cont =
 	lbl_types.(i) <- lbl;
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
-      (* Compilation des corps *)
+      (* Compiling bodies *)
       for i = 0 to ndef - 1 do
 	let params,body = decompose_lam rec_bodies.(i) in
 	let arity = List.length params in
@@ -550,9 +554,9 @@ let rec compile_constr reloc c sz cont =
       let ndef = Array.length type_bodies in
       let lbl_types = Array.create ndef Label.no in
       let lbl_bodies = Array.create ndef Label.no in
-      (* Compilation des types *)
+      (* Compiling types *)
       let rfv = ref empty_fv in
-      let env_type = comp_env_type rfv in
+      let env_type = comp_env_cofix_type ndef rfv in
       for i = 0 to ndef - 1 do
 	let lbl,fcode =
 	  label_code
@@ -560,7 +564,7 @@ let rec compile_constr reloc c sz cont =
 	lbl_types.(i) <- lbl;
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
-      (* Compilation des corps *)
+      (* Compiling bodies *)
       for i = 0 to ndef - 1 do
 	let params,body = decompose_lam rec_bodies.(i) in
 	let arity = List.length params in
@@ -585,11 +589,11 @@ let rec compile_constr reloc c sz cont =
       let lbl_consts = Array.create oib.mind_nb_constant Label.no in
       let lbl_blocks = Array.create (oib.mind_nb_args+1) Label.no in
       let branch1,cont = make_branch cont in
-      (* Compilation du type *)
+      (* Compiling return type *)
       let lbl_typ,fcode =
 	label_code (compile_constr reloc t sz [Kpop sz; Kstop])
       in fun_code := [Ksequence(fcode,!fun_code)];
-      (* Compilation des branches *)
+      (* Compiling branches *)
       let lbl_sw = Label.create () in
       let sz_b,branch,is_tailcall =
 	match branch1 with
@@ -597,13 +601,13 @@ let rec compile_constr reloc c sz cont =
 	| _ -> sz+3, Kjump, false
       in
       let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
-     (* Compilation de la branche accumulate *)
+     (* Compiling branch for accumulators *)
       let lbl_accu, code_accu =
 	label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont)
       in
       lbl_blocks.(0) <- lbl_accu;
       let c = ref code_accu in
-      (* Compilation des branches constructeurs *)
+      (* Compiling regular constructor branches *)
       for i = 0 to Array.length tbl - 1 do
 	let tag, arity = tbl.(i) in
 	if arity = 0 then
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 82bd017a..3f4c1059 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: closure.ml 13340 2010-07-28 12:22:04Z barras $ *)
 
 open Util
 open Pp
@@ -524,6 +524,7 @@ let destFLambda clos_fun t =
     | FLambda(n,(na,ty)::tys,b,e) ->
         (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)})
     | _ -> assert false
+	(* t must be a FLambda and binding list cannot be empty *)
 
 (* Optimization: do not enclose variables in a closure.
    Makes variable access much faster *)
@@ -758,8 +759,8 @@ let rec reloc_rargs_rec depth stk =
 let reloc_rargs depth stk =
   if depth = 0 then stk else reloc_rargs_rec depth stk
 
-let rec drop_parameters depth n stk =
-  match stk with
+let rec drop_parameters depth n argstk =
+  match argstk with
       Zapp args::s ->
         let q = Array.length args in
         if n > q then drop_parameters depth (n-q) s
@@ -768,9 +769,12 @@ let rec drop_parameters depth n stk =
           let aft = Array.sub args n (q-n) in
           reloc_rargs depth (append_stack aft s)
     | Zshift(k)::s -> drop_parameters (depth-k) n s
-    | [] -> assert (n=0); []
-    | _ -> assert false (* we know that n < stack_args_size(stk) *)
-
+    | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
+	if n=0 then []
+	else anomaly
+	  "ill-typed term: found a match on a partially applied constructor"
+    | _ -> assert false
+	(* strip_update_shift_app only produces Zapp and Zshift items *)
 
 (* Iota reduction: expansion of a fixpoint.
  * Given a fixpoint and a substitution, returns the corresponding
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 7d212f53..0af30bed 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: closure.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index ca9482d0..935f6fe7 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: conv_oracle.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Names
 
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 1de1ddbf..94911edd 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: conv_oracle.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index e6bc0684..ad5e725b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: cooking.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Util
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index a471dbc9..bd1f4aec 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: cooking.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 145ca27d..8eeb1ce6 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -146,7 +146,7 @@ and slot_for_fv env fv =
 	    let (_, b, _) = lookup_rel i env.env_rel_context in
 	    let (v, d) =
 	      match b with
-		| None -> (val_of_rel i, Idset.empty)
+		| None -> (val_of_rel (nb_rel env - i), Idset.empty)
 		| Some c -> let renv =  env_of_rel i env in
 			      (val_of_constr renv c, Environ.global_vars_set (Environ.env_of_pre_env renv) c)
 	    in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d3866b42..42055a23 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: declarations.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 56075869..ee1242bb 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: declarations.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/entries.ml b/kernel/entries.ml
index d3dcc5e7..cec46423 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: entries.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 2b3e2c49..ecc50213 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: entries.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 41805241..935faae6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: environ.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ef912e6f..7485ca37 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: environ.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 2ba2670a..2d3956a1 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: esubst.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 2cad93f5..96da8dda 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: esubst.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Explicit substitutions of type ['a]. *)
 (*  - ESID(n)             = %n END   bounded identity
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index df3670d5..91aec40c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: indtypes.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index b9f39cef..8384a63a 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: indtypes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca7d0614..ba5e5252 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: inductive.ml 13368 2010-08-03 13:22:49Z barras $ *)
 
 open Util
 open Names
@@ -418,8 +418,10 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let spec_of_tree t =
-  if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
+let spec_of_tree t = lazy
+  (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec
+   then Not_subterm
+   else Subterm(Strict,Lazy.force t))
 
 let subterm_spec_glb =
   let glb2 s1 s2 =
@@ -443,7 +445,7 @@ type guard_env =
     (* the recarg information of inductive family *)
     recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    genv    : subterm_spec list;
+    genv    : subterm_spec Lazy.t list;
   }
 
 let make_renv env minds recarg (kn,tyi) =
@@ -454,7 +456,7 @@ let make_renv env minds recarg (kn,tyi) =
     rel_min = recarg+2;
     inds = minds;
     recvec = mind_recvec;
-    genv = [Subterm(Large,mind_recvec.(tyi))] }
+    genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] }
 
 let push_var renv (x,ty,spec) =
   { renv with
@@ -466,11 +468,11 @@ let assign_var_spec renv (i,spec) =
   { renv with genv = list_assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
-  push_var renv (x,ty,Not_subterm)
+  push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
 
 (* Fetch recursive information about a variable p *)
 let subterm_var p renv =
-  try List.nth renv.genv (p-1)
+  try Lazy.force (List.nth renv.genv (p-1))
   with Failure _ | Invalid_argument _ -> Not_subterm
 
 (* Add a variable and mark it as strictly smaller with information [spec]. *)
@@ -482,14 +484,14 @@ let push_ctxt_renv renv ctxt =
   { renv with
     env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
   { renv with
     env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
 
 
 (******************************)
@@ -513,12 +515,47 @@ let lookup_subterms env ind =
 
 (*********************************)
 
+let match_trees t1 t2 =
+  let v1 = dest_subterms t1 in
+  let v2 = dest_subterms t2 in
+  array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) v1 v2
+
+(* In {match c as z in ind y_s return P with |C_i x_s => t end}
+   [branches_specif renv c_spec ind] returns an array of x_s specs given
+   c_spec the spec of c. *)
+let branches_specif renv c_spec ind =
+  let (_,mip) = lookup_mind_specif renv.env ind in
+  let car = 
+    (* We fetch the regular tree associated to the inductive of the match.
+       This is just to get the number of constructors (and constructor
+       arities) that fit the match branches without forcing c_spec.
+       Note that c_spec might be more precise than [v] below, because of
+       nested inductive types. *)
+    let v = dest_subterms mip.mind_recargs in
+      Array.map List.length v in
+    Array.mapi
+      (fun i nca -> (* i+1-th cstructor has arity nca *)
+	 let lvra = lazy 
+	   (match Lazy.force c_spec with
+		Subterm (_,t) when match_trees mip.mind_recargs t ->
+		  let vra = Array.of_list (dest_subterms t).(i) in
+		  assert (nca = Array.length vra);
+		  Array.map
+		    (fun t -> Lazy.force (spec_of_tree (lazy t)))
+		    vra
+	      | Dead_code -> Array.create nca Dead_code
+	      | _ -> Array.create nca Not_subterm) in
+	 list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+      car 
+
+
 (* Propagation of size information through Cases: if the matched
    object is a recursive subterm then compute the information
    associated to its own subterms.
    Rq: if branch is not eta-long, then the recursive information
    is not propagated to the missing abstractions *)
 let case_branches_specif renv c_spec ind lbr =
+  let vlrec = branches_specif renv c_spec ind in
   let rec push_branch_args renv lrec c =
     match lrec with
         ra::lr ->
@@ -530,17 +567,8 @@ let case_branches_specif renv c_spec ind lbr =
             | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
                 (renv,c'))
       | [] -> (renv, c) in
-  match c_spec with
-      Subterm (_,t) ->
-        let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Dead_code ->
-        let t = dest_subterms (lookup_subterms renv.env ind) in
-        let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
+  assert (Array.length vlrec = Array.length lbr);
+  array_map2 (push_branch_args renv) vlrec lbr
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
@@ -582,7 +610,8 @@ let rec subterm_specif renv t =
               let renv' =
                 (* Why Strict here ? To be general, it could also be
                    Large... *)
-                assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
+                assign_var_spec renv'
+		  (nbfix-i, Lazy.lazy_from_val(Subterm(Strict,recargs))) in
               let decrArg = recindxs.(i) in
               let theBody = bodies.(i)   in
               let nbOfAbst = decrArg+1 in
@@ -593,7 +622,7 @@ let rec subterm_specif renv t =
                 if List.length l < nbOfAbst then renv''
                 else
                   let theDecrArg  = List.nth l decrArg in
-	          let arg_spec    = subterm_specif renv theDecrArg in
+	          let arg_spec    = lazy_subterm_specif renv theDecrArg in
                   assign_var_spec renv'' (1, arg_spec) in
 	      subterm_specif renv'' strippedBody)
 
@@ -607,10 +636,13 @@ let rec subterm_specif renv t =
     (* Other terms are not subterms *)
     | _ -> Not_subterm
 
+and lazy_subterm_specif renv t =
+  lazy (subterm_specif renv t)
+
 and case_subterm_specif renv ci c lbr =
   if Array.length lbr = 0 then [||]
   else
-    let c_spec = subterm_specif renv c in
+    let c_spec = lazy_subterm_specif renv c in
     case_branches_specif renv c_spec ci.ci_ind lbr
  
 (* Check term c can be applied to one of the mutual fixpoints. *)
@@ -627,7 +659,7 @@ let error_illegal_rec_call renv fx arg =
   let (_,le_vars,lt_vars) =
     List.fold_left
       (fun (i,le,lt) sbt ->
-        match sbt with
+        match Lazy.force sbt with
             (Subterm(Strict,_) | Dead_code) -> (i+1, le, i::lt)
           | (Subterm(Large,_)) -> (i+1, i::le, lt)
           | _ -> (i+1, le ,lt))
@@ -709,7 +741,7 @@ let check_one_fix renv recpos def =
                 (fun j body ->
                   if i=j then
                     let theDecrArg  = List.nth l decrArg in
-	            let arg_spec = subterm_specif renv theDecrArg in
+	            let arg_spec = lazy_subterm_specif renv theDecrArg in
 	            check_nested_fix_body renv' (decrArg+1) arg_spec body
                   else check_rec_call renv' body)
                 bodies
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 59eaf77f..a2bd674f 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: inductive.mli 13368 2010-08-03 13:22:49Z barras $ i*)
 
 (*i*)
 open Names
@@ -110,9 +110,9 @@ type guard_env =
     (* the recarg information of inductive family *)
     recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    genv    : subterm_spec list;
+    genv    : subterm_spec Lazy.t list;
   }
 
 val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec -> inductive ->
+val case_branches_specif : guard_env -> subterm_spec Lazy.t -> inductive ->
   constr array -> (guard_env * constr) array
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index d27fad95..53d26ec6 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: mod_subst.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index f137c7c0..a16ee99e 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: mod_subst.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s [Mod_subst] *)
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d0e567a8..c2a2ffee 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: mod_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 open Names
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 7f35530f..58a80869 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: mod_typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Declarations
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2cac5334..02662adf 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: modops.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/kernel/modops.mli b/kernel/modops.mli
index c1c262cc..9b12fea6 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: modops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/kernel/names.ml b/kernel/names.ml
index 54304376..550c70b4 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: names.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/kernel/names.mli b/kernel/names.mli
index 8209119c..f54df6ec 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: names.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Identifiers *)
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index f35da2d2..bad04af5 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pre_env.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index ac51e49d..80f382c6 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pre_env.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cd4902c5..00e8014f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: reduction.ml 13354 2010-07-29 16:44:45Z barras $ *)
 
 open Util
 open Names
@@ -253,7 +253,8 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
     | (FAtom a1, FAtom a2) ->
 	(match kind_of_term a1, kind_of_term a2 with
 	   | (Sort s1, Sort s2) ->
-	       assert (is_empty_stack v1 && is_empty_stack v2);
+	       if not (is_empty_stack v1 && is_empty_stack v2) then
+		 anomaly "conversion was given ill-typed terms (Sort)";
 	       sort_cmp cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if n=m
@@ -313,14 +314,16 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
 
     (* other constructors *)
     | (FLambda _, FLambda _) ->
-        assert (is_empty_stack v1 && is_empty_stack v2);
+        if not (is_empty_stack v1 && is_empty_stack v2) then
+	  anomaly "conversion was given ill-typed terms (FLambda)";
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
         let u1 = ccnv CONV infos el1 el2 ty1 ty2 cuniv in
         ccnv CONV infos (el_lift el1) (el_lift el2) bd1 bd2 u1
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
-        assert (is_empty_stack v1 && is_empty_stack v2);
+        if not (is_empty_stack v1 && is_empty_stack v2) then
+	  anomaly "conversion was given ill-typed terms (FProd)";
 	(* Luo's system *)
         let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
         ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 28691fa1..83a858cf 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: reduction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 69c830e7..799bce47 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: retroknowledge.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term
 open Names
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index c0854361..2a4878e9 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: retroknowledge.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f8154f19..dee2f5e8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: safe_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 0443dcf2..446ee75b 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: safe_typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 44b35970..0d4887ec 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: sign.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Names
 open Util
diff --git a/kernel/sign.mli b/kernel/sign.mli
index f470377b..313118e4 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: sign.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f8cbd840..cbff43ad 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: subtyping.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index 32bca5df..d3736fd9 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: subtyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Univ
diff --git a/kernel/term.ml b/kernel/term.ml
index 4c0a8890..b031f750 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: term.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index f1e78246..f9e11df5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: term.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8054eff7..8cd9b909 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: term_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index b731f813..4d32be1e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: term_typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 65a9d76a..033dde90 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: type_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Names
 open Term
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index f93ddb6c..38ee5058 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: type_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index ee29da42..7527e3e7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: typeops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a3ec5a64..aaacf3c5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: typeops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 03550cbd..77c14b10 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: univ.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index d71c4832..da01879c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: univ.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Universes. *)
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 35032c6b..ceb8ea9c 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: vm.ml 13363 2010-07-30 16:17:24Z barras $ *)
 
 open Names
 open Term
@@ -16,7 +16,7 @@ open Cbytecodes
 external set_drawinstr : unit -> unit = "coq_set_drawinstr"
 
 (******************************************)
-(* Fonctions en plus du module Obj ********)
+(* Utility Functions about Obj ************)
 (******************************************)
 
 external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
@@ -25,7 +25,7 @@ external offset : Obj.t -> int = "coq_offset"
 let accu_tag = 0
 
 (*******************************************)
-(* Initalisation de la machine abstraite ***)
+(* Initalization of the abstract machine ***)
 (*******************************************)
 
 external init_vm : unit -> unit = "init_coq_vm"
@@ -36,15 +36,13 @@ external transp_values : unit -> bool = "get_coq_transp_value"
 external set_transp_values : bool -> unit = "coq_set_transp_value"
 
 (*******************************************)
-(* Le code machine  ************************)
+(* Machine code *** ************************)
 (*******************************************)
 
 type tcode
 let tcode_of_obj v = ((Obj.obj v):tcode)
 let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0)
 
-
-
 external mkAccuCode : int -> tcode = "coq_makeaccu"
 external mkPopStopCode : int -> tcode = "coq_pushpop"
 external mkAccuCond : int -> tcode = "coq_accucond"
@@ -73,12 +71,12 @@ let popstop_code i =
 let stop = popstop_code 0
 
 (******************************************************)
-(* Types de donnees abstraites et fonctions associees *)
+(* Abstract data types and utility functions **********)
 (******************************************************)
 
 (* Values of the abstract machine *)
 let val_of_obj v = ((Obj.obj v):values)
-let crasy_val = (val_of_obj (Obj.repr 0))
+let crazy_val = (val_of_obj (Obj.repr 0))
 
 (* Abstract data *)
 type vprod
@@ -99,63 +97,60 @@ type vswitch = {
     sw_env : vm_env
   }
 
-(* Representation des types abstraits:                                    *)
-(* + Les produits :                                                       *)
+(* Representation of values *)
+(* + Products : *)
 (*   -   vprod = 0_[ dom | codom]                                         *)
 (*             dom : values, codom : vfun                                 *)
 (*                                                                        *)
-(* + Les fonctions ont deux representations possibles :                   *)
-(*   - fonction non applique :  vf = Ct_[ C | fv1 | ... | fvn]            *)
+(* + Functions have two representations :                                 *)
+(*   - unapplied fun :  vf = Ct_[ C | fv1 | ... | fvn]                    *)
 (*                                       C:tcode, fvi : values            *)
-(*     Remarque : il n'y a pas de difference entre la fct et son          *)
-(*                environnement.                                          *)
-(*   - Application partielle  : Ct_[Restart:C| vf | arg1 | ... argn]      *)
+(*     Remark : a function and its environment is the same value.         *)
+(*   - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn]       *)
 (*                                                                        *)
-(* + Les points fixes :                                                   *)
+(* + Fixpoints :                                                          *)
 (*   -        Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn]               *)
-(*     Remarque il n'y a qu'un seul block pour representer tout les       *)
-(*     points fixes d'une declaration mutuelle, chaque point fixe         *)
-(*     pointe sur la position de son code dans le block.                  *)
-(*   - L'application partielle d'un point fixe suit le meme schema        *)
-(*     que celui des fonctions                                            *)
-(*     Remarque seul les points fixes qui n'ont pas encore recu leur      *)
-(*     argument recursif sont encode de cette maniere (si l'argument      *)
-(*     recursif etait un constructeur le point fixe se serait reduit      *)
-(*     sinon il est represente par un accumulateur)                       *)
+(*     One single block to represent all of the fixpoints, each fixpoint  *)
+(*     is the pointer to the field holding the pointer to its code, and   *)
+(*     the infix tag is used to know where the block starts.              *)
+(*   - Partial application follows the scheme of partially applied        *)
+(*     functions. Note: only fixpoints not having been applied to its     *)
+(*     recursive argument are coded this way. When the rec. arg. is       *)
+(*     applied, either it's a constructor and the fix reduces, or it's    *)
+(*     and the fix is coded as an accumulator.                            *)
 (*                                                                        *)
-(* + Les cofix sont expliques dans cbytegen.ml                            *)
+(* + Cofixpoints : see cbytegen.ml                                        *)
 (*                                                                        *)
-(* + Les vblock encodent les constructeurs (non constant) de caml,        *)
-(*   la difference est que leur tag commence a 1 (0 est reserve pour les  *)
-(*   accumulateurs : accu_tag)                                            *)
+(* + vblock's encode (non constant) constructors as in Ocaml, but         *)
+(*   starting from 0 up. tag 0 ( = accu_tag) is reserved for              *)
+(*   accumulators.                                                        *)
 (*                                                                        *)
-(* + vm_env est le type des environnement machine (une fct ou un pt fixe) *)
+(* + vm_env is the type of the machine environments (i.e. a function or   *)
+(*   a fixpoint)                                                          *)
 (*                                                                        *)
-(* + Les accumulateurs : At_[accumulate| accu | arg1 | ... | argn ]       *)
-(*   - representation des [accu] : tag_[....]                             *)
-(*     -- tag <= 2 : encodage du type atom                                *)
-(*     -- 3_[accu|fix_app] : un point fixe bloque par un accu             *)
-(*     -- 4_[accu|vswitch] : un case bloque par un accu                   *)
-(*     -- 5_[fcofix]       : une fonction de cofix                        *)
-(*     -- 6_[fcofix|val]   : une fonction de cofix, val represente        *)
-(*        la valeur de la reduction de la fct applique a arg1 ... argn    *)
-(* Le type [arguments] est utiliser de maniere abstraite comme un         *)
-(* tableau, il represente la structure de donnee suivante :               *)
+(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
+(*   - representation of [accu] : tag_[....]                              *)
+(*     -- tag <= 2 : encoding atom type (sorts, free vars, etc.)          *)
+(*     -- 3_[accu|fix_app] : a fixpoint blocked by an accu                *)
+(*     -- 4_[accu|vswitch] : a match blocked by an accu                   *)
+(*     -- 5_[fcofix]       : a cofix function                             *)
+(*     -- 6_[fcofix|val]   : a cofix function, val represent the value    *)
+(*        of the function applied to arg1 ... argn                        *)
+(* The [arguments] type, which is abstracted as an array, represents :    *)
 (*          tag[ _ | _ |v1|... | vn]                                      *)
-(* Generalement le 1er champs est un pointeur de code                     *)
+(* Generally the first field is a code pointer.                           *)
 
-(* Ne pas changer ce type sans modifier le code C, *)
-(* en particulier le fichier "coq_values.h"        *)
+(* Do not edit this type without editing C code, especially "coq_values.h" *)
 type atom =
   | Aid of id_key
   | Aiddef of id_key * values
   | Aind of inductive
 
-(* Les zippers *)
+(* Zippers *)
 
 type zipper =
   | Zapp of arguments
-  | Zfix of vfix*arguments  (* Peut-etre vide *)
+  | Zfix of vfix*arguments  (* Possibly empty *)
   | Zswitch of vswitch
 
 type stack = zipper list
@@ -193,28 +188,20 @@ let rec whd_accu a stk =
       let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
       whd_accu (Obj.field at 0) (zswitch :: stk)
   | 5 (* cofix_tag *) ->
+      let vcfx = Obj.obj (Obj.field at 0) in
+      let to_up = Obj.obj a in
       begin match stk with
-      | [] ->
-	  let vcfx = Obj.obj (Obj.field at 0) in
-	  let to_up = Obj.obj a in
-	  Vcofix(vcfx, to_up, None)
-      | [Zapp args] ->
-	  let vcfx = Obj.obj (Obj.field at 0) in
-	  let to_up = Obj.obj a in
-	  Vcofix(vcfx, to_up, Some args)
+      | []          -> Vcofix(vcfx, to_up, None)
+      | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
       | _           -> assert false
       end
   | 6 (* cofix_evaluated_tag *) ->
+      let vcofix = Obj.obj (Obj.field at 0) in
+      let res = Obj.obj a in
       begin match stk with
-      | [] ->
-	  let vcofix = Obj.obj (Obj.field at 0) in
-	  let res = Obj.obj a in
-	  Vcofix(vcofix, res, None)
-      | [Zapp args] ->
-	  let vcofix = Obj.obj (Obj.field at 0) in
-	  let res = Obj.obj a in
-	  Vcofix(vcofix, res, Some args)
-      | _ -> assert false
+      | []          -> Vcofix(vcofix, res, None)
+      | [Zapp args] -> Vcofix(vcofix, res, Some args)
+      | _           -> assert false
       end
   | _ -> assert false
 
@@ -245,7 +232,7 @@ let whd_val : values -> whd =
 
 
 (************************************************)
-(* La machine abstraite *************************)
+(* Abstrct machine ******************************)
 (************************************************)
 
 (* gestion de la pile *)
@@ -291,7 +278,7 @@ let apply_vstack vf vstk =
     end
 
 (**********************************************)
-(* Constructeurs ******************************)
+(* Constructors *******************************)
 (**********************************************)
 
 let obj_of_atom : atom -> Obj.t =
@@ -349,11 +336,11 @@ let mkrel_vstack k arity =
   let max = k + arity - 1 in
   Array.init arity (fun i -> val_of_rel (max - i))
 
+
 (*************************************************)
-(** Operations pour la manipulation des donnees **)
+(** Operations manipulating data types ***********)
 (*************************************************)
 
-
 (* Functions over products *)
 
 let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0)
@@ -395,13 +382,13 @@ exception FALSE
 
 let check_fix f1 f2 =
   let i1, i2 = current_fix f1, current_fix f2 in
-  (* Verification du point de depart *)
+  (* Checking starting point *)
   if i1 = i2 then
     let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
     let n = Obj.size (last fb1) in
-    (* Verification du nombre de definition *)
+    (* Checking number of definitions *)
     if n = Obj.size (last fb2) then
-      (* Verification des arguments recursifs *)
+      (* Checking recursive arguments *)
       try
 	for i = 0 to n - 1 do
 	  if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i
@@ -439,14 +426,14 @@ let relaccu_code i =
 
 let reduce_fix k vf =
   let fb = first (Obj.repr vf) in
-  (* calcul des types *)
+  (* computing types *)
   let fc_typ = ((Obj.obj (last fb)) : tcode array) in
   let ndef = Array.length fc_typ in
   let et = offset_closure fb (2*(ndef - 1)) in
   let ftyp =
     Array.map
-      (fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in
-  (* Construction de l' environnement des corps des points fixes *)
+      (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in
+  (* Construction of the environment of fix bodies *)
   let e = Obj.dup fb in
   for i = 0 to ndef - 1 do
     Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i)))
@@ -485,9 +472,10 @@ let reduce_cofix k vcf =
   let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in
   let ndef = Array.length fc_typ in
   let ftyp =
-    Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in
-  (* Construction de l'environnement des corps des cofix *)
+    (* Evaluate types *)
+    Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in
 
+  (* Construction of the environment of cofix bodies *)
   let e = Obj.dup (Obj.repr vcf) in
   for i = 0 to ndef - 1 do
     Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))
@@ -522,7 +510,7 @@ let case_info sw = sw.sw_annot.ci
 
 let type_of_switch sw =
   push_vstack sw.sw_stk;
-  interprete sw.sw_type_code crasy_val sw.sw_env 0
+  interprete sw.sw_type_code crazy_val sw.sw_env 0
 
 let branch_arg k (tag,arity) =
   if arity = 0 then  ((Obj.magic tag):values)