Changement des named_context

Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs


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

26 files changed, 401 insertions, 374 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 48d91e4dc..8bfe78ebe 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -55,7 +55,7 @@ sp is a local copy of the global variable extern_sp. */
 #  define Next break
 #endif 
 
-/*#define _COQ_DEBUG_ */
+/* #define _COQ_DEBUG_ */
 
 #ifdef _COQ_DEBUG_ 
 #   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
@@ -715,7 +715,7 @@ value coq_interprete
 	  forcable = Val_true;
 	  /* On pousse l'addresse de retour et l'argument */
 	  sp -= 3;
-	  sp[0] = (value) (pc);
+	  sp[0] = (value) (pc - 1);
 	  sp[1] = coq_env;
 	  sp[2] = Val_long(coq_extra_args);
 	  /* On evalue le cofix */
@@ -966,6 +966,7 @@ value coq_push_vstack(value stk) {
 value  coq_interprete_ml(value tcode, value a, value e, value ea) {
   print_instr("coq_interprete");
   return coq_interprete((code_t)tcode, a, e, Long_val(ea));
+   print_instr("end coq_interprete");
 }
 
 value coq_eval_tcode (value tcode, value e) {
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index cc59558e1..041e0795d 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -4,7 +4,7 @@ open Cbytecodes
 open Cemitcodes
 open Term
 open Declarations
-open Environ
+open Pre_env
 
 (*i Compilation des variables + calcul des variables libres *)
 
@@ -191,7 +191,7 @@ let get_strcst = function
 let rec str_const c =
   match kind_of_term c with
   | Sort s -> Bstrconst (Const_sorts s)
-  | Cast(c,_) -> str_const c 
+  | Cast(c,_,_) -> str_const c 
   | App(f,args) -> 
       begin
 	match kind_of_term f with
@@ -201,18 +201,18 @@ let rec str_const c =
 	    let num,arity = oip.mind_reloc_tbl.(i-1) in
 	    let nparams = oib.mind_nparams in
 	    if nparams + arity = Array.length args then
-	    if arity = 0 then Bstrconst(Const_b0 num)
-	    else
-	      let rargs = Array.sub args nparams arity in
-	      let b_args = Array.map str_const rargs in
-	      try 
-		let sc_args = Array.map get_strcst b_args in
-		Bstrconst(Const_bn(num, sc_args))
-	      with Not_found ->
-		Bmakeblock(num,b_args)
+	      if arity = 0 then Bstrconst(Const_b0 num)
+	      else
+		let rargs = Array.sub args nparams arity in
+		let b_args = Array.map str_const rargs in
+		try 
+		  let sc_args = Array.map get_strcst b_args in
+		  Bstrconst(Const_bn(num, sc_args))
+		with Not_found ->
+		  Bmakeblock(num,b_args)
 	    else  
-	    let b_args = Array.map str_const args in
-	    Bconstruct_app(num, nparams, arity, b_args)
+	      let b_args = Array.map str_const args in
+	      Bconstruct_app(num, nparams, arity, b_args)
 	| _ -> Bconstr c
       end
   | Ind ind -> Bstrconst (Const_ind ind)
@@ -274,7 +274,7 @@ let rec compile_constr reloc c sz cont =
   | Meta _ -> raise (Invalid_argument "Cbytegen.gen_lam : Meta")
   | Evar _ -> raise (Invalid_argument "Cbytegen.gen_lam : Evar")
  
-  | Cast(c,_) -> compile_constr reloc c sz cont
+  | Cast(c,_,_) -> compile_constr reloc c sz cont
 
   | Rel i -> pos_rel i reloc sz :: cont
   | Var id -> pos_named id reloc :: cont
@@ -483,10 +483,6 @@ let compile_constant_body env body opaque boxed =
       else
 	match kind_of_term body with
 	| Const kn' -> BCallias (get_allias env kn')
-	| Construct _ ->
-	    let res = compile env body in
-	    let to_patch = to_memory res in
-	    BCdefined (false, to_patch)
 	| _ -> 
 	    let res = compile env body in
 	    let to_patch = to_memory res in
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 135afb1e2..f761e4f60 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -3,7 +3,7 @@ open Cbytecodes
 open Cemitcodes 
 open Term
 open Declarations
-open Environ
+open Pre_env
 
 
 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index b79168785..625d3b0d0 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -357,22 +357,22 @@ let ref_value_cache info ref =
 
 let defined_vars flags env =
 (*  if red_local_const (snd flags) then*)
-    fold_named_context 
-      (fun env (id,b,t) e ->
+    Sign.fold_named_context 
+      (fun (id,b,_) e ->
 	 match b with
 	   | None -> e
 	   | Some body -> (id, body)::e)
-      env ~init:[]
+       (named_context env) ~init:[]
 (*  else []*)
 
 let defined_rels flags env =
 (*  if red_local_const (snd flags) then*)
-  fold_rel_context 
-      (fun env (id,b,t) (i,subs) ->
+  Sign.fold_rel_context 
+      (fun (id,b,t) (i,subs) ->
 	 match b with
 	   | None -> (i+1, subs)
 	   | Some body -> (i+1, (i,body) :: subs))
-      env ~init:(0,[])
+      (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
 
@@ -512,7 +512,7 @@ type fconstr = {
 and fterm =
   | FRel of int
   | FAtom of constr (* Metas and Sorts *)
-  | FCast of fconstr * fconstr
+  | FCast of fconstr * cast_kind * fconstr
   | FFlex of table_key
   | FInd of inductive
   | FConstruct of constructor
@@ -603,10 +603,10 @@ let rec compact_constr (lg, subs as s) c k =
     | Evar(ev,v) ->
         let (v',s) = compact_vect s v k in
         if v==v' then c,s else mkEvar(ev,v'),s
-    | Cast(a,b) ->
+    | Cast(a,ck,b) ->
         let (a',s) = compact_constr s a k in
         let (b',s) = compact_constr s b k in
-        if a==a' && b==b' then c,s else mkCast(a',b'), s
+        if a==a' && b==b' then c,s else mkCast(a', ck, b'), s
     | App(f,v) ->
         let (f',s) = compact_constr s f k in
         let (v',s) = compact_vect s v k in
@@ -693,9 +693,9 @@ let mk_clos_deep clos_fun env t =
   match kind_of_term t with
     | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) ->
         mk_clos env t
-    | Cast (a,b) ->
+    | Cast (a,k,b) ->
         { norm = Red;
-          term = FCast (clos_fun env a, clos_fun env b)}
+          term = FCast (clos_fun env a, k, clos_fun env b)}
     | App (f,v) ->
         { norm = Red;
 	  term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
@@ -728,8 +728,8 @@ let rec to_constr constr_fun lfts v =
     | FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
     | FFlex (VarKey x) -> mkVar x
     | FAtom c -> exliftn lfts c
-    | FCast (a,b) ->
-        mkCast (constr_fun lfts a, constr_fun lfts b)
+    | FCast (a,k,b) ->
+        mkCast (constr_fun lfts a, k, constr_fun lfts b)
     | FFlex (ConstKey op) -> mkConst op
     | FInd op -> mkInd op
     | FConstruct op -> mkConstruct op
@@ -976,7 +976,7 @@ let rec knh m stk =
         (match get_nth_arg m ri.(n) stk with
              (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk')
            | (None, stk') -> (m,stk'))
-    | FCast(t,_) -> knh t stk
+    | FCast(t,_,_) -> knh t stk
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
        FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) ->
@@ -990,7 +990,7 @@ and knht e t stk =
     | Case(ci,p,t,br) ->
         knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
     | Fix _ -> knh (mk_clos2 e t) stk
-    | Cast(a,b) -> knht e a stk
+    | Cast(a,_,_) -> knht e a stk
     | Rel n -> knh (clos_rel e n) stk
     | (Lambda _|Prod _|Construct _|CoFix _|Ind _|
        LetIn _|Const _|Var _|Evar _|Meta _|Sort _) ->
diff --git a/kernel/closure.mli b/kernel/closure.mli
index e394b15b8..4c0f9d32e 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -130,7 +130,7 @@ type fconstr
 type fterm =
   | FRel of int
   | FAtom of constr (* Metas and Sorts *)
-  | FCast of fconstr * fconstr
+  | FCast of fconstr * cast_kind * fconstr 
   | FFlex of table_key
   | FInd of inductive
   | FConstruct of constructor
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index f743970c6..fc2d09254 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -4,12 +4,9 @@ open Vm
 open Cemitcodes
 open Cbytecodes
 open Declarations
-open Environ
+open Pre_env
 open Cbytegen
-open Cemitcodes
-
 
-open Format 
 
 external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
 external free_tcode : tcode -> unit = "coq_static_free"
@@ -78,6 +75,17 @@ let str_cst_tbl = Hashtbl.create 31
 let annot_tbl = Hashtbl.create 31
     (* (annot_switch * int) Hashtbl.t  *)
 
+(*************************************************************)
+(*** Mise a jour des valeurs des variables et des constantes *)
+(*************************************************************)
+
+exception NotEvaluated
+
+let key rk =
+  match !rk with
+  | Some k -> k
+  | _ -> raise NotEvaluated
+
 (************************)
 (* traduction des patch *)
 
@@ -98,55 +106,46 @@ let slot_for_annot key =
     Hashtbl.add annot_tbl key n;
     n
 
-open Format
-
 let rec slot_for_getglobal env kn =
-  let ck = lookup_constant_key kn env in
-  try constant_key_pos ck
+  let (cb,rk) = lookup_constant_key kn env in
+  try key rk
   with NotEvaluated ->
-    match force (constant_key_body ck).const_body_code with
-    | BCdefined(boxed,(code,pl,fv)) -> 
+    let pos =
+      match Cemitcodes.force cb.const_body_code with
+      | BCdefined(boxed,(code,pl,fv)) -> 
 	let v = eval_to_patch env (code,pl,fv) in
-   	let pos = 
-	  if boxed then set_global_boxed kn v 
-	  else set_global v in
-	set_pos_constant ck pos;
-	pos
-    | BCallias kn' ->
-	let pos = slot_for_getglobal env kn' in
-	set_pos_constant ck pos;
-	pos
-    | BCconstant -> 
-	let v = val_of_constant kn in
-	let pos = set_global v in
-	set_pos_constant ck pos;
-	pos  
+  	if boxed then set_global_boxed kn v 
+	else set_global v 
+    | BCallias kn' -> slot_for_getglobal env kn' 
+    | BCconstant -> set_global (val_of_constant kn) in
+    rk := Some pos;
+    pos
 
 and slot_for_fv env fv=
   match fv with
   | FVnamed id -> 
-      let nv = lookup_namedval id env in
+      let nv = lookup_named_val id env in
       begin
-	match kind_of_named nv with
+	match !nv with
 	| VKvalue v -> v
 	| VKaxiom id ->
 	    let v = val_of_named id in
-	    set_namedval nv v; v
-	| VKdef(c,e) ->
-	    let v = val_of_constr e c in
-	    set_namedval nv v; v
+	    nv := VKvalue v; v
+	| VKdef c ->
+	    let v = val_of_constr (env_of_named id env) c in
+	    nv := VKvalue v; v
       end
   | FVrel i ->
-      let rv = lookup_relval i env in
+      let rv = lookup_rel_val i env in
       begin
-	match kind_of_rel rv with
+	match !rv with
 	| VKvalue v -> v
 	| VKaxiom k ->
 	    let v = val_of_rel k in
-	    set_relval rv v; v
-	| VKdef(c,e) ->
-	    let v = val_of_constr e c in
-	    set_relval rv v; v
+	    rv := VKvalue v; v
+	| VKdef c ->
+	    let v = val_of_constr (env_of_rel i env) c in
+	    rv := VKvalue v; v
       end
  
 and eval_to_patch env (buff,pl,fv) = 
@@ -164,7 +163,7 @@ and eval_to_patch env (buff,pl,fv) =
 and val_of_constr env c = 
   let (_,fun_code,_ as ccfv) = 
     try compile env c 
-    with e -> print_string "can not compile \n";print_flush();raise e in
+    with e -> print_string "can not compile \n";Format.print_flush();raise e in
   eval_to_patch env (to_memory ccfv)
  
 let set_transparent_const kn =
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 4c56fc947..2640a4df1 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -1,6 +1,6 @@
 open Names
 open Term
-open Environ
+open Pre_env
 
 val val_of_constr : env -> constr -> values 
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9ce925207..82864bbe4 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -20,6 +20,9 @@ open Mod_subst
 (* This module defines the types of global declarations. This includes
    global constants/axioms and mutual inductive definitions *)
 
+type engagement = ImpredicativeSet
+
+
 (*s Constants (internal representation) (Definition/Axiom) *)
 
 type constr_substituted = constr substituted
@@ -191,3 +194,4 @@ and module_body =
       mod_type : module_type_body;
       mod_equiv : module_path option;
       mod_constraints : constraints }
+
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 62a1cc07c..cdb394380 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -21,6 +21,9 @@ open Mod_subst
    declarations. This includes global constants/axioms, mutual
    inductive definitions, modules and module types *)
 
+type engagement = ImpredicativeSet
+
+
 (*s Constants (Definition/Axiom) *)
 
 type constr_substituted
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6d16632cd..45ae911a2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -14,76 +14,31 @@ open Sign
 open Univ
 open Term
 open Declarations
+open Pre_env
+open Csymtable
 
 (* The type of environments. *)
 
-type checksum = int
+type named_context_val = Pre_env.named_context_val
 
-type compilation_unit_name = dir_path * checksum
+type env = Pre_env.env
 
-type global = Constant | Inductive
-
-type key = int option ref 
-type constant_key = constant_body * key
- 
-type engagement = ImpredicativeSet
-
-type globals = {
-  env_constants : constant_key Cmap.t;
-  env_inductives : mutual_inductive_body KNmap.t;
-  env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body KNmap.t }
-
-type stratification = {
-  env_universes : universes;
-  env_engagement : engagement option
-}
-
-type 'a val_kind =   
-  | VKvalue of values
-  | VKaxiom of 'a
-  | VKdef of constr * env
-
-and 'a lazy_val = 'a val_kind ref
-
-and env = {
-  env_globals       : globals;
-  env_named_context : named_context;
-  env_named_val     : (identifier * (identifier lazy_val)) list;
-  env_rel_context   : rel_context;
-  env_rel_val       : inv_rel_key lazy_val list;
-  env_nb_rel        : int;
-  env_stratification : stratification }
-
-let empty_env = { 
-  env_globals = {
-    env_constants = Cmap.empty;
-    env_inductives = KNmap.empty;
-    env_modules = MPmap.empty;
-    env_modtypes = KNmap.empty };
-  env_named_context = empty_named_context;
-  env_named_val = [];
-  env_rel_context = empty_rel_context;
-  env_rel_val = [];
-  env_nb_rel = 0;
-  env_stratification = {
-    env_universes = initial_universes;
-    env_engagement = None } }
+let pre_env env = env
 
+let empty_named_context_val = empty_named_context_val
 
+let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
+let named_context_val env = env.env_named_context,env.env_named_vals
 let rel_context env = env.env_rel_context
 
 let empty_context env = 
   env.env_rel_context = empty_rel_context 
   && env.env_named_context = empty_named_context
 
-exception NotEvaluated 
-exception AllReadyEvaluated
-
 (* Rel context *)
 let lookup_rel n env =
   Sign.lookup_rel n env.env_rel_context
@@ -98,18 +53,7 @@ let evaluable_rel n env =
 
 let nb_rel env = env.env_nb_rel
 
-let push_rel d env =
-  let _,body,_ = d in
-  let rval =
-    match body with
-    | None -> ref (VKaxiom env.env_nb_rel)
-    | Some c -> ref (VKdef(c,env))
-  in     
-  { env with
-    env_rel_context = add_rel_decl d env.env_rel_context;
-    env_rel_val = rval :: env.env_rel_val;
-    env_nb_rel = env.env_nb_rel + 1 }
- 
+let push_rel = push_rel
 
 let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
     
@@ -126,105 +70,87 @@ let reset_rel_context env =
     env_nb_rel = 0 }
 
 let fold_rel_context f env ~init =
-  snd (Sign.fold_rel_context
-	 (fun d (env,e) -> (push_rel d env, f env d e))
-         (rel_context env) ~init:(reset_rel_context env,init))
-    
-(* Abstract machine rel values *)
-type relval = int lazy_val
-      
-let kind_of_rel r = !r
-    
-let set_relval r v =
-  match !r with
-  | VKvalue _ -> raise AllReadyEvaluated
-  | _ -> r := VKvalue v
-	
-let lookup_relval n env =
-  try List.nth env.env_rel_val (n - 1)
-  with _ -> raise Not_found
-      
+  let rec fold_right env =
+    match env.env_rel_context with
+    | [] -> init
+    | rd::rc ->
+	let env = 
+	  { env with
+	    env_rel_context = rc;
+	    env_rel_val = List.tl env.env_rel_val;
+	    env_nb_rel = env.env_nb_rel - 1 } in
+	f env rd (fold_right env) 
+  in fold_right env
+
 (* Named context *)
-let lookup_named id env =
-  Sign.lookup_named id env.env_named_context
-    
+
+let named_context_of_val = fst
+
+(* [map_named_val f ctxt] apply [f] to the body and the type of
+   each declarations.
+   *** /!\ ***   [f t] should be convertible with t *)  
+let map_named_val f (ctxt,ctxtv) = 
+  let ctxt =
+    List.map (fun (id,body,typ) -> (id, option_app f body, f typ)) ctxt in
+  (ctxt,ctxtv)
+
+let empty_named_context = empty_named_context 
+
+let push_named = push_named
+let push_named_context_val = push_named_context_val
+
+let val_of_named_context ctxt =
+  List.fold_right push_named_context_val ctxt empty_named_context_val
+
+
+let lookup_named id env = Sign.lookup_named id env.env_named_context
+let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt
 
 (* A local const is evaluable if it is defined  *)
+
+let named_type id env =
+  let (_,_,t) = lookup_named id env in t
+
+let named_body id env =
+  let (_,b,_) = lookup_named id env in b
+
 let evaluable_named id env =
   try 
-    match lookup_named id env with
-      (_,Some _,_) -> true
-    | _ -> false
-  with Not_found -> 
-    false
+    match named_body id env with
+    |Some _      -> true
+    | _          -> false
+  with Not_found -> false
       
-let push_named d env = 
-  let id,body,_ = d in
-  let rval =
-    match body with
-    | None -> ref (VKaxiom id)
-    | Some c -> ref (VKdef(c,env))
-	  
-  in
-  { env with  
-    env_named_context = Sign.add_named_decl d env.env_named_context;
-    env_named_val =  (id,rval):: env.env_named_val }
-
-let reset_context env =
+let reset_with_named_context (ctxt,ctxtv) env =
   { env with
-    env_named_context = empty_named_context;
-    env_named_val = [];
+    env_named_context = ctxt;
+    env_named_vals = ctxtv;
     env_rel_context = empty_rel_context;
     env_rel_val = [];
     env_nb_rel = 0 }
 
-let reset_with_named_context ctxt env =
-  Sign.fold_named_context push_named ctxt ~init:(reset_context env)
-    
+let reset_context = reset_with_named_context empty_named_context_val
+ 
 let fold_named_context f env ~init =
-  snd (Sign.fold_named_context
-	 (fun d (env,e) -> (push_named d env, f env d e))
-         (named_context env) ~init:(reset_context env,init))
-    
+  let rec fold_right env =
+    match env.env_named_context with
+    | [] -> init
+    | d::ctxt ->
+	let env = 
+	  reset_with_named_context (ctxt,List.tl env.env_named_vals) env in
+	f env d (fold_right env) 
+  in fold_right env
+
 let fold_named_context_reverse f ~init env =
-  Sign.fold_named_context_reverse f ~init:init (named_context env) 
-    
-(* Abstract machine values of local vars referred by names *)
-type namedval = identifier lazy_val
-
-let kind_of_named r = !r
-
-let set_namedval r v =
-  match !r with
-  | VKvalue _ -> raise AllReadyEvaluated
-  | _ -> r := VKvalue v
-	
-let lookup_namedval id env =
-  snd (List.find (fun (id',_) -> id = id') env.env_named_val)
-  
+  Sign.fold_named_context_reverse f ~init:init (named_context env)
+ 
 (* Global constants *)
 
-let notevaluated = None
-    
-let constant_key_pos (cb,r) =
-  match !r with
-  | None -> raise NotEvaluated
-  | Some key -> key
-
-let constant_key_body = fst 
-
-let set_pos_constant (cb,r) bpos =
-  if !r = notevaluated then r := Some bpos 
-  else raise AllReadyEvaluated
-
-let lookup_constant_key kn env =
-  Cmap.find kn env.env_globals.env_constants
-
-let lookup_constant kn env = constant_key_body (lookup_constant_key kn env)
+let lookup_constant = lookup_constant
 
 let add_constant kn cs env =
   let new_constants = 
-    Cmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in
+    Cmap.add kn (cs,ref None) env.env_globals.env_constants in
   let new_globals = 
     { env.env_globals with 
 	env_constants = new_constants } in 
@@ -256,8 +182,7 @@ let evaluable_constant cst env =
   with Not_found | NotEvaluableConst _ -> false
 
 (* Mutual Inductives *)
-let lookup_mind kn env =
-  KNmap.find kn env.env_globals.env_inductives
+let lookup_mind = lookup_mind
 
 let add_mind kn mib env =
   let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
@@ -341,7 +266,6 @@ let keep_hyps env needed =
     (named_context env)
     ~init:empty_named_context
 
-
 (* Modules *)
 
 let add_modtype ln mtb env = 
@@ -381,3 +305,61 @@ type unsafe_type_judgment = {
   utj_val : constr;
   utj_type : sorts }
 
+(*s Compilation of global declaration *)
+
+let compile_constant_body = Cbytegen.compile_constant_body  
+
+(*s Special functions for the refiner (logic.ml) *)
+
+let clear_hyps ids check (ctxt,vals) =
+  let ctxt,vals,rmv = 
+    List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) ->
+      if List.mem id ids then (ctxt,vals,id::rmv)
+      else begin
+	check rmv d;
+	(d::ctxt,v::vals,rmv)
+      end) ctxt vals ([],[],[])
+  in ((ctxt,vals),rmv)
+
+exception Hyp_not_found
+
+let rec apply_to_hyp (ctxt,vals) id f =
+  let rec aux rtail ctxt vals =
+    match ctxt, vals with
+    | (idc,c,ct as d)::ctxt, v::vals ->
+	if idc = id then
+	  (f ctxt d rtail)::ctxt, v::vals
+	else 
+	  let ctxt',vals' = aux (d::rtail) ctxt vals in
+	  d::ctxt', v::vals'
+    | [],[] -> raise Hyp_not_found
+    | _, _ -> assert false
+  in aux [] ctxt vals
+
+let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
+  let rec aux ctxt vals =
+    match ctxt,vals with
+    | (idc,c,ct as d)::ctxt, v::vals ->
+	if idc = id then
+	  let sign = ctxt,vals in
+	  push_named_context_val (f d sign) sign 
+	else 
+	  let (ctxt,vals as sign) = aux ctxt vals in
+	  push_named_context_val (g d sign) sign
+    | [],[] -> raise Hyp_not_found
+    | _,_ -> assert false
+  in aux ctxt vals
+
+let insert_after_hyp (ctxt,vals) id d check =
+  let rec aux ctxt vals =
+    match  ctxt, vals with
+    | (idc,c,ct as d')::ctxt', v::vals' ->
+	if idc = id then begin
+	  check ctxt; 
+	  push_named_context_val d (ctxt,vals) 
+	end else 
+	  let ctxt,vals = aux ctxt vals in
+	  d::ctxt, v::vals
+    | [],[] -> raise Hyp_not_found
+    | _, _ -> assert false
+  in aux ctxt vals
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 20027d32a..b8f565e45 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -30,15 +30,20 @@ open Sign
    - a set of universe constraints
    - a flag telling if Set is, can be, or cannot be set impredicative *)
 
+
+
+
 type env
+val pre_env : env -> Pre_env.env
+
+type named_context_val
 
 val empty_env : env
 
 val universes     : env -> Univ.universes
 val rel_context   : env -> rel_context
 val named_context : env -> named_context
-
-type engagement = ImpredicativeSet
+val named_context_val : env -> named_context_val
 
 val engagement    : env -> engagement option
 
@@ -47,6 +52,7 @@ val empty_context : env -> bool
 
 (************************************************************************)
 (*s Context of de Bruijn variables ([rel_context]) *)
+val nb_rel           : env -> int 
 val push_rel         : rel_declaration -> env -> env
 val push_rel_context :     rel_context -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
@@ -56,39 +62,41 @@ val push_rec_types   : rec_declaration -> env -> env
 val lookup_rel    : int -> env -> rel_declaration
 val evaluable_rel : int -> env -> bool
 
-(* Abstract machine rel values *)
-type 'a val_kind =   
-  | VKvalue of values
-  | VKaxiom of 'a
-  | VKdef of constr * env
-
-type relval
-
-val kind_of_rel : relval -> inv_rel_key val_kind
-val set_relval : relval -> values -> unit
-val lookup_relval : int -> env -> relval
-val nb_rel : env -> int
 (*s Recurrence on [rel_context] *)
 val fold_rel_context :
   (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (************************************************************************)
 (* Context of variables (section variables and goal assumptions) *)
+
+val named_context_of_val : named_context_val -> named_context
+val val_of_named_context : named_context -> named_context_val
+val empty_named_context_val : named_context_val
+
+
+(* [map_named_val f ctxt] apply [f] to the body and the type of
+   each declarations.
+   *** /!\ ***   [f t] should be convertible with t *)  
+val map_named_val : 
+   (constr -> constr) -> named_context_val -> named_context_val
+
 val push_named : named_declaration -> env -> env
+val push_named_context_val  : 
+    named_declaration -> named_context_val -> named_context_val
+
+
 
 (* Looks up in the context of local vars referred by names ([named_context]) *)
 (* raises [Not_found] if the identifier is not found *)
-val lookup_named    : variable -> env -> named_declaration
-val evaluable_named : variable -> env -> bool
 
-(* Abstract machine values of local vars referred by names *)
-type namedval
-
-val kind_of_named : namedval -> identifier val_kind
-val set_namedval : namedval -> values -> unit
-val lookup_namedval : identifier -> env -> namedval
+val lookup_named     : variable -> env -> named_declaration
+val lookup_named_val : variable -> named_context_val -> named_declaration
+val evaluable_named  : variable -> env -> bool
+val named_type : variable -> env -> types
+val named_body : variable -> env -> constr option
  
 (*s Recurrence on [named_context]: older declarations processed first *)
+
 val fold_named_context :
   (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
@@ -99,7 +107,7 @@ val fold_named_context_reverse :
 (* This forgets named and rel contexts *)
 val reset_context : env -> env
 (* This forgets rel context and sets a new named context *)
-val reset_with_named_context : named_context -> env -> env
+val reset_with_named_context : named_context_val -> env -> env
 
 (************************************************************************)
 (*s Global constants *)
@@ -108,15 +116,7 @@ val add_constant : constant -> constant_body -> env -> env
 
 (* Looks up in the context of global constant names *)
 (* raises [Not_found] if the required path is not found *)
-type constant_key 
-exception NotEvaluated
-exception AllReadyEvaluated
 
-val constant_key_pos : constant_key -> int  
-val constant_key_body : constant_key -> constant_body
-val set_pos_constant : constant_key -> int -> unit
-
-val lookup_constant_key : constant -> env -> constant_key
 val lookup_constant    : constant -> env -> constant_body
 val evaluable_constant : constant -> env -> bool
 
@@ -183,7 +183,35 @@ type unsafe_type_judgment = {
   utj_type : sorts }
 
 
+(*s Compilation of global declaration *)
+
+val compile_constant_body : 
+    env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
+                                 (* opaque *) (* boxed *)
+
+(*s Functions for proofs/logic.ml *)
+val clear_hyps : 
+    variable list -> (variable list -> named_declaration -> unit) -> 
+      named_context_val -> named_context_val * variable list
+
+exception Hyp_not_found
 
+(* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
+   return [tail::(f head (id,_,_) (rev tail))::head].
+   the value associated to id should not change *)
 
+val apply_to_hyp : named_context_val -> variable -> 
+  (named_context -> named_declaration -> named_context -> named_declaration) ->
+    named_context_val
 
+(* [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
+   [tail::(id,_,_)::head] and
+   return [(g tail)::(f (id,_,_))::head]. *)
+val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
+  (named_declaration -> named_context_val -> named_declaration) ->
+    (named_declaration -> named_context_val -> named_declaration) ->
+      named_context_val
 
+val insert_after_hyp : named_context_val -> variable ->
+  named_declaration -> 
+    (named_context -> unit) -> named_context_val
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 218d7f822..d12c3a213 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -132,7 +132,7 @@ let rec infos_and_sort env t =
 	let logic = not (is_info_type env varj) in
 	let small = Term.is_small varj.utj_type in
 	(logic,small) :: (infos_and_sort env1 c2)
-    | Cast (c,_) -> infos_and_sort env c
+    | Cast (c,_,_) -> infos_and_sort env c
     | _ -> []
 
 let small_unit constrsinfos =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b5d825e84..af237d1d1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -630,7 +630,7 @@ let check_one_fix renv recpos def =
 
       (* The cases below simply check recursively the condition on the
          subterms *)
-      | Cast (a,b) -> 
+      | Cast (a,_, b) -> 
           List.for_all (check_rec_call renv) (a::b::l)
 
       | Lambda (x,a,b) ->
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index bb3027aa8..efbee6af2 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -97,7 +97,7 @@ and merge_with env mtb with_decl =
 			SPBconst {cb with 
 				    const_body = body;
 			            const_body_code = Cemitcodes.from_val
-                        (Cbytegen.compile_constant_body env' body false false);
+                        (compile_constant_body env' body false false);
                                     const_constraints = cst}
 		  | Some b -> 
 		      let cst1 = Reduction.conv env' c (Declarations.force b) in
@@ -106,7 +106,7 @@ and merge_with env mtb with_decl =
 			SPBconst {cb with 
 				    const_body = body;
 				    const_body_code = Cemitcodes.from_val
-                        (Cbytegen.compile_constant_body env' body false false);
+                        (compile_constant_body env' body false false);
                                     const_constraints = cst}
 	      end	
 (* and what about msid's ????? Don't they clash ? *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 7b4c3095d..b20e7259d 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -257,7 +257,7 @@ let strengthen_const env mp l cb =
       	   const_body = const_subs;
 	   const_opaque = false;
            const_body_code = Cemitcodes.from_val
-             (Cbytegen.compile_constant_body env const_subs false false)
+             (compile_constant_body env const_subs false false)
 	}
 
 let strengthen_mind env mp l mib = match mib.mind_equiv with
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 156e3a44a..2467e941f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -342,31 +342,28 @@ let conv_leq_vecti env v1 v2 =
 
 (* option for conversion *)
 
-let vm_fconv = ref fconv 
-
-let set_default_vm_conv _ = vm_fconv := fconv
-let set_vm_conv_cmp f = vm_fconv := f
-
+let vm_conv = ref fconv
+let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 = 
   try 
-    !vm_fconv cv_pb env t1 t2
+    !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
       clos_fconv cv_pb env t1 t2
   
 
-let vm_conv_leq_vecti env v1 v2 =
-  array_fold_left2_i 
-    (fun i c t1 t2 ->
-      let c' =
-        try vm_conv CUMUL env t1 t2 
-        with NotConvertible -> raise (NotConvertibleVect i) in
-      Constraint.union c c')
-    Constraint.empty
-    v1
-    v2
+let default_conv = ref fconv 
 
-let vm_conv_leq = vm_conv CUMUL
+let set_default_conv f = default_conv := f
+
+let default_conv cv_pb env t1 t2 = 
+  try 
+    !default_conv cv_pb env t1 t2
+  with Not_found | Invalid_argument _ ->
+      (* If compilation fails, fall-back to closure conversion *)
+      clos_fconv cv_pb env t1 t2
+  
+let default_conv_leq = default_conv CUMUL
 (*
 let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
 let conv_leq env t1 t2 =
@@ -419,7 +416,7 @@ let dest_prod_assum env =
     | LetIn (x,b,t,c) ->
         let d = (x,Some b,t) in
 	prodec_rec (push_rel d env) (Sign.add_rel_decl d l) c
-    | Cast (c,_)    -> prodec_rec env l c
+    | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> l,rty
   in
   prodec_rec env Sign.empty_rel_context
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 5d383e61e..60cd999d8 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -44,12 +44,12 @@ val conv_leq       : types conversion_function
 val conv_leq_vecti : types array conversion_function
 
 (* option for conversion *)
-
-val set_default_vm_conv : unit -> unit
-val set_vm_conv_cmp : (conv_pb -> types conversion_function) -> unit
+val set_vm_conv : (conv_pb -> types conversion_function) -> unit
 val vm_conv : conv_pb -> types conversion_function
-val vm_conv_leq_vecti : types array conversion_function
-val vm_conv_leq          : types conversion_function
+
+val set_default_conv : (conv_pb -> types conversion_function) -> unit
+val default_conv     : conv_pb -> types conversion_function
+val default_conv_leq : types conversion_function
 
 (************************************************************************)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 83aa3e943..5412287ee 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -67,7 +67,7 @@ val add_constraints :
   Univ.constraints -> safe_environment -> safe_environment
 
 (* Settin the strongly constructive or classical logical engagement *)
-val set_engagement : Environ.engagement -> safe_environment -> safe_environment
+val set_engagement : engagement -> safe_environment -> safe_environment
 
 
 (*s Interactive module functions *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index a90b43335..dd22d5b8c 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -122,7 +122,7 @@ let destArity =
     match kind_of_term c with
     | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
     | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
-    | Cast (c,_)      -> prodec_rec l c
+    | Cast (c,_,_)      -> prodec_rec l c
     | Sort s          -> l,s
     | _               -> anomaly "destArity: not an arity"
   in 
@@ -134,7 +134,7 @@ let rec isArity c =
   match kind_of_term c with
   | Prod (_,_,c)    -> isArity c
   | LetIn (_,b,_,c) -> isArity (subst1 b c)
-  | Cast (c,_)      -> isArity c
+  | Cast (c,_,_)      -> isArity c
   | Sort _          -> true
   | _               -> false
 
@@ -145,7 +145,7 @@ let decompose_prod_assum =
     match kind_of_term c with
     | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) c
     | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c
-    | Cast (c,_)      -> prodec_rec l c
+    | Cast (c,_,_)      -> prodec_rec l c
     | _               -> l,c
   in 
   prodec_rec empty_rel_context
@@ -157,7 +157,7 @@ let decompose_lam_assum =
     match kind_of_term c with
     | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) c
     | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c
-    | Cast (c,_)      -> lamdec_rec l c
+    | Cast (c,_,_)      -> lamdec_rec l c
     | _               -> l,c
   in 
   lamdec_rec empty_rel_context
@@ -172,7 +172,7 @@ let decompose_prod_n_assum n =
     else match kind_of_term c with 
     | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
     | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
-    | Cast (c,_)      -> prodec_rec l n c
+    | Cast (c,_,_)      -> prodec_rec l n c
     | c -> error "decompose_prod_n_assum: not enough assumptions"
   in 
   prodec_rec empty_rel_context n
@@ -187,7 +187,7 @@ let decompose_lam_n_assum n =
     else match kind_of_term c with 
     | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
     | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
-    | Cast (c,_)      -> lamdec_rec l n c
+    | Cast (c,_,_)      -> lamdec_rec l n c
     | c -> error "decompose_lam_n_assum: not enough abstractions"
   in 
   lamdec_rec empty_rel_context n 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 5ab9f9a02..0c339e8b8 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -134,7 +134,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
     let rec names_prod_letin t = match kind_of_term t with 
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)
-      | Cast(t,_) -> names_prod_letin t
+      | Cast(t,_,_) -> names_prod_letin t
       | _ -> []
     in 
     assert (Array.length mib1.mind_packets = 1);
diff --git a/kernel/term.ml b/kernel/term.ml
index 8bd079ce5..f59ba5d66 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -21,6 +21,8 @@ open Esubst
 type existential_key = int
 type metavariable = int
 
+(* This defines the strategy to use for verifiying a Cast *)
+
 (* This defines Cases annotations *)
 type pattern_source = DefaultPat of int | RegularPat
 type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
@@ -56,6 +58,8 @@ let family_of_sort = function
 (*       Constructions as implemented                               *)
 (********************************************************************)
 
+type cast_kind = VMcast | DEFAULTcast 
+
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type 'constr pexistential = existential_key * 'constr array
@@ -74,7 +78,7 @@ type ('constr, 'types) kind_of_term =
   | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
-  | Cast      of 'constr * 'types
+  | Cast      of 'constr * cast_kind * 'types
   | Prod      of name * 'types * 'types
   | Lambda    of name * 'types * 'constr
   | LetIn     of name * 'constr * 'types * 'constr
@@ -89,14 +93,14 @@ type ('constr, 'types) kind_of_term =
 (* Experimental *)
 type ('constr, 'types) kind_of_type =
   | SortType   of sorts
-  | CastType   of 'types * 'types
+  | CastType   of 'types * 'types 
   | ProdType   of name * 'types * 'types
   | LetInType  of name * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
 
 let kind_of_type = function
   | Sort s -> SortType s
-  | Cast (c,t) -> CastType (c, t)
+  | Cast (c,_,t) -> CastType (c, t)
   | Prod (na,t,c) -> ProdType (na, t, c)
   | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
   | App (c,l) -> AtomicType (c, l)
@@ -123,7 +127,7 @@ let comp_term t1 t2 =
   | Meta m1, Meta m2 -> m1 == m2
   | Var id1, Var id2 -> id1 == id2
   | Sort s1, Sort s2 -> s1 == s2
-  | Cast (c1,t1), Cast (c2,t2) -> c1 == c2 & t1 == t2
+  | Cast (c1,_,t1), Cast (c2,_,t2) -> c1 == c2 & t1 == t2
   | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
   | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
   | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) ->
@@ -154,7 +158,7 @@ let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t =
   | Meta x -> Meta x
   | Var x -> Var (sh_id x)
   | Sort s -> Sort (sh_sort s)
-  | Cast (c,t) -> Cast (sh_rec c, sh_rec t)
+  | Cast (c, k, t) -> Cast (sh_rec c, k, (sh_rec t))
   | Prod (na,t,c) -> Prod (sh_na na, sh_rec t, sh_rec c)
   | Lambda (na,t,c) -> Lambda (sh_na na, sh_rec t, sh_rec c)
   | LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
@@ -207,11 +211,12 @@ let mkVar id = Var id
 let mkSort s = Sort s
 
 (* 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) *)
-let mkCast (t1,t2) =
+(* (that means t2 is declared as the type of t1) 
+   [s] is the strategy to use when *)
+let mkCast (t1,k2,t2) =
   match t1 with
-    | Cast (t,_) -> Cast (t,t2)
-    | _ -> Cast (t1,t2)
+  | Cast (c,k1, _) when k1 = k2 -> Cast (c,k1,t2)
+  | _ -> Cast (t1,k2,t2)
 
 (* Constructs the product (x:t1)t2 *)
 let mkProd (x,t1,t2) = Prod (x,t1,t2)
@@ -310,22 +315,22 @@ let destSort c = match kind_of_term c with
 
 let rec isprop c = match kind_of_term c with
   | Sort (Prop _) -> true
-  | Cast (c,_) -> isprop c
+  | Cast (c,_,_) -> isprop c
   | _ -> false
 
 let rec is_Prop c = match kind_of_term c with
   | Sort (Prop Null) -> true
-  | Cast (c,_) -> is_Prop c
+  | Cast (c,_,_) -> is_Prop c
   | _ -> false
 
 let rec is_Set c = match kind_of_term c with
   | Sort (Prop Pos) -> true
-  | Cast (c,_) -> is_Set c
+  | Cast (c,_,_) -> is_Set c
   | _ -> false
 
 let rec is_Type c = match kind_of_term c with
   | Sort (Type _) -> true
-  | Cast (c,_) -> is_Type c
+  | Cast (c,_,_) -> is_Type c
   | _ -> false
 
 let isType = function
@@ -345,10 +350,11 @@ let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false
 
 (* Destructs a casted term *)
 let destCast c = match kind_of_term c with 
-  | Cast (t1, t2) -> (t1,t2)
+  | Cast (t1,k,t2) -> (t1,k,t2)
   | _ -> invalid_arg "destCast"
 
-let isCast c = match kind_of_term c with Cast (_,_) -> true | _ -> false
+let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
+
 
 (* Tests if a de Bruijn index *)
 let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
@@ -434,7 +440,7 @@ let rec collapse_appl c = match kind_of_term c with
   | App (f,cl) -> 
       let rec collapse_rec f cl2 = match kind_of_term f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-	| Cast (c,_) when isApp c -> collapse_rec c cl2
+	| Cast (c,_,_) when isApp c -> collapse_rec c cl2
 	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
@@ -450,11 +456,11 @@ let rec strip_head_cast c = match kind_of_term c with
   | App (f,cl) -> 
       let rec collapse_rec f cl2 = match kind_of_term f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-	| Cast (c,_) -> collapse_rec c cl2
+	| Cast (c,_,_) -> collapse_rec c cl2
 	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
-  | Cast (c,t) -> strip_head_cast c
+  | Cast (c,_,_) -> strip_head_cast c
   | _ -> c
 
 (****************************************************************************)
@@ -468,7 +474,7 @@ let rec strip_head_cast c = match kind_of_term c with
 let fold_constr f acc c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
-  | Cast (c,t) -> f (f acc c) t
+  | Cast (c,_,t) -> f (f acc c) t
   | Prod (_,t,c) -> f (f acc t) c
   | Lambda (_,t,c) -> f (f acc t) c
   | LetIn (_,b,t,c) -> f (f (f acc b) t) c
@@ -489,7 +495,7 @@ let fold_constr f acc c = match kind_of_term c with
 let iter_constr f c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
-  | Cast (c,t) -> f c; f t
+  | Cast (c,_,t) -> f c; f t
   | Prod (_,t,c) -> f t; f c
   | Lambda (_,t,c) -> f t; f c
   | LetIn (_,b,t,c) -> f b; f t; f c
@@ -508,7 +514,7 @@ let iter_constr f c = match kind_of_term c with
 let iter_constr_with_binders g f n c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
-  | Cast (c,t) -> f n c; f n t
+  | Cast (c,_,t) -> f n c; f n t
   | Prod (_,t,c) -> f n t; f (g n) c
   | Lambda (_,t,c) -> f n t; f (g n) c
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
@@ -529,7 +535,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with
 let map_constr f c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
-  | Cast (c,t) -> mkCast (f c, f t)
+  | Cast (c,k,t) -> mkCast (f c, k, f t)
   | Prod (na,t,c) -> mkProd (na, f t, f c)
   | Lambda (na,t,c) -> mkLambda (na, f t, f c)
   | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
@@ -550,7 +556,7 @@ let map_constr f c = match kind_of_term c with
 let map_constr_with_binders g f l c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
-  | Cast (c,t) -> mkCast (f l c, f l t)
+  | Cast (c,k,t) -> mkCast (f l c, k, f l t)
   | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c)
   | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
   | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
@@ -575,8 +581,8 @@ let compare_constr f t1 t2 =
   | Meta m1, Meta m2 -> m1 = m2
   | Var id1, Var id2 -> id1 = id2
   | Sort s1, Sort s2 -> s1 = s2
-  | Cast (c1,_), _ -> f c1 t2
-  | _, Cast (c2,_) -> f t1 c2
+  | Cast (c1,_,_), _ -> f c1 t2
+  | _, Cast (c2,_,_) -> f t1 c2
   | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2
   | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
   | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
@@ -607,6 +613,8 @@ let compare_constr f t1 t2 =
 
 type types = constr
 
+type strategy = types option 
+
 let type_app f tt = f tt
 
 let body_of_type ty = ty
@@ -673,7 +681,7 @@ let noccur_with_meta n m term =
     | Rel p -> if n<=p & p<n+m then raise LocalOccur
     | App(f,cl) ->
 	(match kind_of_term f with
-           | Cast (c,_) when isMeta c -> ()
+           | Cast (c,_,_) when isMeta c -> ()
            | Meta _ -> ()
 	   | _ -> iter_constr_with_binders succ occur_rec n c)
     | Evar (_, _) -> ()
@@ -942,17 +950,17 @@ let implicit_sort = Type (make_univ(make_dirpath[id_of_string"implicit"],0))
 let mkImplicit = mkSort implicit_sort
 
 let rec strip_outer_cast c = match kind_of_term c with
-  | Cast (c,_) -> strip_outer_cast c
+  | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
 
 (* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
 
 let under_outer_cast f c =  match kind_of_term c with
-  | Cast (b,t) -> mkCast (f b,f t)
+  | Cast (b,k,t) -> mkCast (f b, k, f t)
   | _ -> f c
 
 let rec under_casts f c = match kind_of_term c with
-  | Cast (c,t) -> mkCast (under_casts f c, t)
+  | Cast (c,k,t) -> mkCast (under_casts f c, k, t)
   | _            -> f c
 
 (***************************)
@@ -1003,7 +1011,7 @@ let rec to_lambda n prod =
   else 
     match kind_of_term prod with 
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
-      | Cast (c,_) -> to_lambda n c
+      | Cast (c,_,_) -> to_lambda n c
       | _   -> errorlabstrm "to_lambda" (mt ())                      
 
 let rec to_prod n lam =
@@ -1012,7 +1020,7 @@ let rec to_prod n lam =
   else   
     match kind_of_term lam with 
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
-      | Cast (c,_) -> to_prod n c
+      | Cast (c,_,_) -> to_prod n c
       | _   -> errorlabstrm "to_prod" (mt ())                      
 	    
 (* pseudo-reduction rule:
@@ -1042,7 +1050,7 @@ let prod_applist t nL = List.fold_left prod_app t nL
 let decompose_prod = 
   let rec prodec_rec l c = match kind_of_term c with
     | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
-    | Cast (c,_)   -> prodec_rec l c
+    | Cast (c,_,_)   -> prodec_rec l c
     | _              -> l,c
   in 
   prodec_rec []
@@ -1052,7 +1060,7 @@ let decompose_prod =
 let decompose_lam = 
   let rec lamdec_rec l c = match kind_of_term c with
     | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
-    | Cast (c,_)     -> lamdec_rec l c
+    | Cast (c,_,_)     -> lamdec_rec l c
     | _                -> l,c
   in 
   lamdec_rec []
@@ -1065,7 +1073,7 @@ let decompose_prod_n n =
     if n=0 then l,c 
     else match kind_of_term c with 
       | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
-      | Cast (c,_)   -> prodec_rec l n c
+      | Cast (c,_,_)   -> prodec_rec l n c
       | _ -> error "decompose_prod_n: not enough products"
   in 
   prodec_rec [] n 
@@ -1078,7 +1086,7 @@ let decompose_lam_n n =
     if n=0 then l,c 
     else match kind_of_term c with 
       | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
-      | Cast (c,_)     -> lamdec_rec l n c
+      | Cast (c,_,_)     -> lamdec_rec l n c
       | _ -> error "decompose_lam_n: not enough abstractions"
   in 
   lamdec_rec [] n 
@@ -1088,7 +1096,7 @@ let decompose_lam_n n =
 let nb_lam = 
   let rec nbrec n c = match kind_of_term c with
     | Lambda (_,_,c) -> nbrec (n+1) c
-    | Cast (c,_) -> nbrec n c
+    | Cast (c,_,_) -> nbrec n c
     | _ -> n
   in 
   nbrec 0
@@ -1097,7 +1105,7 @@ let nb_lam =
 let nb_prod = 
   let rec nbrec n c = match kind_of_term c with
     | Prod (_,_,c) -> nbrec (n+1) c
-    | Cast (c,_) -> nbrec n c
+    | Cast (c,_,_) -> nbrec n c
     | _ -> n
   in 
   nbrec 0
diff --git a/kernel/term.mli b/kernel/term.mli
index 9c8f2fa10..70388808a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -12,6 +12,7 @@
 open Names
 (*i*)
 
+
 (*s The sorts of CCI. *)
 
 type contents = Pos | Null
@@ -99,9 +100,13 @@ val mkProp : types
 val mkSet  : types
 val mkType : Univ.universe -> types
 
+
+(* This defines the strategy to use for verifiying a Cast *)
+type cast_kind = VMcast | DEFAULTcast 
+
 (* Constructs the term [t1::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 * types -> constr
+val mkCast : constr * cast_kind * constr -> constr
 
 (* Constructs the product [(x:t1)t2] *)
 val mkProd : name * types * types -> types
@@ -192,7 +197,7 @@ type ('constr, 'types) kind_of_term =
   | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
-  | Cast      of 'constr * 'types
+  | Cast      of 'constr * cast_kind * 'types
   | Prod      of name * 'types * 'types
   | Lambda    of name * 'types * 'constr
   | LetIn     of name * 'constr * 'types * 'constr
@@ -213,7 +218,7 @@ val kind_of_term : constr -> (constr, types) kind_of_term
 (* Experimental *)
 type ('constr, 'types) kind_of_type =
   | SortType   of sorts
-  | CastType   of 'types * 'types
+  | CastType   of 'types * 'types 
   | ProdType   of name * 'types * 'types
   | LetInType  of name * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
@@ -258,7 +263,7 @@ val destVar : constr -> identifier
 val destSort : constr -> sorts
 
 (* Destructs a casted term *)
-val destCast : constr -> constr * types
+val destCast : constr -> constr * cast_kind * constr
 
 (* Destructs the product $(x:t_1)t_2$ *)
 val destProd : types -> name * types * types
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b62e7b007..f76c5ffe3 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -19,8 +19,6 @@ open Inductive
 open Environ
 open Entries
 open Type_errors
-open Cemitcodes
-open Cbytegen
 open Indtypes
 open Typeops
 
@@ -28,13 +26,10 @@ let constrain_type env j cst1 = function
   | None -> j.uj_type, cst1
   | Some t -> 
       let (tj,cst2) = infer_type env t in
-      let cst3 =
-	try vm_conv_leq env j.uj_type tj.utj_val
-	with NotConvertible -> error_actual_type env j tj.utj_val in
+      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
       assert (t = tj.utj_val);
       t, Constraint.union (Constraint.union cst1 cst2) cst3
 
-
 let translate_local_def env (b,topt) =
   let (j,cst) = infer env b in
   let (typ,cst) = constrain_type env j cst topt in
@@ -99,7 +94,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) =
 	  (global_vars_set env (Declarations.force b)) 
 	  (global_vars_set env typ)
   in
-  let tps = from_val (compile_constant_body env body op boxed) in
+  let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
   let hyps = keep_hyps env ids in
     { const_hyps = hyps;
       const_body = body;
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a70d81e66..3a968545f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -19,10 +19,20 @@ open Entries
 open Reduction
 open Inductive
 open Type_errors
-
-let conv = vm_conv CONV
-let conv_leq = vm_conv CUMUL
-let conv_leq_vecti = vm_conv_leq_vecti
+  
+let conv = default_conv CONV
+let conv_leq = default_conv CUMUL
+
+let conv_leq_vecti env v1 v2 =
+  array_fold_left2_i 
+    (fun i c t1 t2 ->
+      let c' =
+        try default_conv CUMUL env t1 t2 
+        with NotConvertible -> raise (NotConvertibleVect i) in
+      Constraint.union c c')
+    Constraint.empty
+    v1
+    v2
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env j =
@@ -89,7 +99,7 @@ let judge_of_relative env n =
 (* Type of variables *)
 let judge_of_variable env id =
   try
-    let (_,_,ty) = lookup_named id env in
+    let ty = named_type id env in
     make_judge (mkVar id) ty
   with Not_found -> 
     error_unbound_var env id
@@ -100,10 +110,9 @@ let judge_of_variable env id =
    variables of the current env *)
 (* TODO: check order? *)
 let rec check_hyps_inclusion env sign =
-  let env_sign = named_context env in
   Sign.fold_named_context
     (fun (id,_,ty1) () ->
-      let (_,_,ty2) = Sign.lookup_named id env_sign in
+      let ty2 = named_type id env in
       if not (eq_constr ty2 ty1) then
         error "types do not match")
     sign
@@ -233,11 +242,14 @@ let judge_of_product env name t1 t2 =
          env |- c:typ2
 *)
 
-let judge_of_cast env cj tj =
+let judge_of_cast env cj k tj =
   let expected_type = tj.utj_val in
   try 
-    let cst = conv_leq env cj.uj_type expected_type in
-    { uj_val = mkCast (j_val cj, expected_type);
+    let cst = 
+      match k with
+      | VMcast -> vm_conv CUMUL env cj.uj_type expected_type
+      | DEFAULTcast -> conv_leq env cj.uj_type expected_type in
+    { uj_val = mkCast (cj.uj_val, k, expected_type);
       uj_type = expected_type },
     cst
   with NotConvertible ->
@@ -279,11 +291,11 @@ let judge_of_constructor env cstr
 
 (* Case. *)
 
-let check_branch_types env cj (lft,explft) = 
-  try conv_leq_vecti env lft explft
+let check_branch_types env cj (lfj,explft) = 
+  try conv_leq_vecti env (Array.map j_type lfj) explft
   with
       NotConvertibleVect i ->
-        error_ill_formed_branch env cj.uj_val i lft.(i) explft.(i)
+        error_ill_formed_branch env cj.uj_val i lfj.(i).uj_type explft.(i)
     | Invalid_argument _ ->
         error_number_branches env cj (Array.length explft)
 
@@ -294,8 +306,7 @@ let judge_of_case env ci pj cj lfj =
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty,univ) =
     type_case_branches env indspec pj cj.uj_val in
-  let lft = Array.map j_type lfj in
-  let univ' = check_branch_types env cj (lft,bty) in
+  let univ' = check_branch_types env cj (lfj,bty) in
   ({ uj_val  = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val,
                        Array.map j_val lfj);
      uj_type = rslty },
@@ -316,9 +327,7 @@ let type_fixpoint env lna lar vdefj =
   let lt = Array.length vdefj in
   assert (Array.length lar = lt);
   try
-    conv_leq_vecti env
-      (Array.map (fun j -> body_of_type j.uj_type) vdefj)
-      (Array.map (fun ty -> lift lt ty) lar)
+    conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar)
   with NotConvertibleVect i ->
     error_ill_typed_rec_body env i lna vdefj lar
 
@@ -375,17 +384,17 @@ let rec execute env cstr cu =
     | LetIn (name,c1,c2,c3) ->
         let (j1,cu1) = execute env c1 cu in
         let (j2,cu2) = execute_type env c2 cu1 in
-        let (_,cu3) = univ_combinator cu2 (judge_of_cast env j1 j2) in
+        let (_,cu3) = 
+	  univ_combinator cu2 (judge_of_cast env j1 DEFAULTcast j2) in
         let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
         let (j',cu4) = execute env1 c3 cu3 in
         (judge_of_letin env name j1 j2 j', cu4)
 	  
-    | Cast (c,t) ->
+    | Cast (c,k, t) ->
         let (cj,cu1) = execute env c cu in
         let (tj,cu2) = execute_type env t cu1 in
 	univ_combinator cu2
-          (judge_of_cast env cj tj)
-
+          (judge_of_cast env cj k tj)
     (* Inductive types *)
     | Ind ind ->
 	(judge_of_inductive env ind, cu)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a537d793e..ed90c393e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -69,8 +69,8 @@ val judge_of_letin :
 
 (*s Type of a cast. *)
 val judge_of_cast :
-  env -> unsafe_judgment -> unsafe_type_judgment
-    -> unsafe_judgment * constraints
+  env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment ->
+    unsafe_judgment * constraints
 
 (*s Inductive types. *)
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 8a2ced1d2..921cd7128 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -6,11 +6,11 @@ open Conv_oracle
 open Reduction 
 open Closure
 open Vm
-open Csymtable
+open Csymtable 
 open Univ
-open Cbytecodes
-
 
+let val_of_constr env c =
+  val_of_constr (pre_env env) c
 
 (* Test la structure des piles *)
 
@@ -194,8 +194,8 @@ let rec conv_eq pb t1 t2 cu =
     | Var id1, Var id2 -> 
 	if id1 = id2 then cu else raise NotConvertible
     | Sort s1, Sort s2 -> sort_cmp pb s1 s2 cu
-    | Cast (c1,_), _ -> conv_eq pb c1 t2 cu
-    | _, Cast (c2,_) -> conv_eq pb t1 c2 cu
+    | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu
+    | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu
     | Prod (_,t1,c1), Prod (_,t2,c2) -> 
 	conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu)
     | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu
@@ -244,12 +244,14 @@ let vconv pb env t1 t2 =
       cu
   in cu
     
-let use_vm = ref true
-let _ = Reduction.set_vm_conv_cmp vconv
+let _ = Reduction.set_vm_conv vconv
+
+let use_vm = ref false
+
 let set_use_vm b =
   use_vm := b;
-  if b then Reduction.set_vm_conv_cmp vconv
-  else Reduction.set_default_vm_conv ()
+  if b then Reduction.set_default_conv vconv
+  else Reduction.set_default_conv Reduction.conv_cmp
       
 let use_vm _ = !use_vm
 
@@ -540,8 +542,6 @@ and nf_cofix env cf =
   let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in
   mkCoFix (init,(name,cft,cfb))
   
-
-
 let cbv_vm env c t  =
   let transp = transp_values () in
   if not transp then set_transp_values true;