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

22 files changed, 170 insertions, 117 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 33a9272d04..8042bff548 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -186,7 +186,7 @@ let rec norm_head info env t stack =
       let nargs = Array.map (cbv_stack_term info TOP env) args in
       norm_head info env head (stack_app (Array.to_list nargs) stack)
   | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
-  | Cast (ct,_) -> norm_head info env ct stack
+  | Cast (ct,_,_) -> norm_head info env ct stack
 
   (* constants, axioms
    * the first pattern is CRUCIAL, n=0 happens very often:
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index cc3725210d..6c4dbf5ed8 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -78,7 +78,7 @@ let clenv_environments evd bound c =
   let rec clrec (e,metas) n c =
     match n, kind_of_term c with
       | (Some 0, _) -> (e, List.rev metas, c)
-      | (n, Cast (c,_)) -> clrec (e,metas) n c
+      | (n, Cast (c,_,_)) -> clrec (e,metas) n c
       | (n, Prod (na,c1,c2)) ->
 	  let mv = new_meta () in
 	  let dep = dependent (mkRel 1) c2 in
@@ -96,7 +96,7 @@ let clenv_environments_evars env evd bound c =
   let rec clrec (e,ts) n c =
     match n, kind_of_term c with
       | (Some 0, _) -> (e, List.rev ts, c)
-      | (n, Cast (c,_)) -> clrec (e,ts) n c
+      | (n, Cast (c,_,_)) -> clrec (e,ts) n c
       | (n, Prod (na,c1,c2)) ->
           let e',constr = Evarutil.new_evar e env c1 in
 	  let dep = dependent (mkRel 1) c2 in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8b6e476c74..19c5ca54be 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -177,7 +177,7 @@ let lookup_name_as_renamed env t s =
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (Anonymous,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
-    | Cast (c,_) -> lookup avoid env_names n c
+    | Cast (c,_,_) -> lookup avoid env_names n c
     | _ -> None
   in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t
 
@@ -191,7 +191,7 @@ let lookup_index_as_renamed env t n =
 	  (match concrete_name true [] empty_names_context name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
-    | Cast (c,_) -> lookup n d c
+    | Cast (c,_,_) -> lookup n d c
     | _ -> None
   in lookup n 1 t
 
@@ -345,8 +345,8 @@ let rec detype tenv avoid env t =
 	  RVar (dummy_loc, id))
     | Sort (Prop c) -> RSort (dummy_loc,RProp c)
     | Sort (Type u) -> RSort (dummy_loc,RType (Some u))
-    | Cast (c1,c2) ->
-	RCast(dummy_loc,detype tenv avoid env c1,
+    | Cast (c1,k,c2) ->
+	RCast(dummy_loc,detype tenv avoid env c1, k,
               detype tenv avoid env c2)
     | Prod (na,ty,c) -> detype_binder tenv BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder tenv BLambda avoid env na ty c
@@ -468,7 +468,7 @@ and detype_eqn tenv avoid env constr construct_nargs branch =
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
             buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
 
-	| Cast (c,_) ->    (* Oui, il y a parfois des cast *)
+	| Cast (c,_,_) ->    (* Oui, il y a parfois des cast *)
 	    buildrec ids patlist avoid env n c
 
 	| _ -> (* eta-expansion : n'arrivera plus lorsque tous les
@@ -600,10 +600,10 @@ let rec subst_raw subst raw =
   | RHole (loc, (BinderType _ | QuestionMark | CasesType |
       InternalHole | TomatchTypeParameter _)) -> raw
 
-  | RCast (loc,r1,r2) -> 
+  | RCast (loc,r1,k,r2) -> 
       let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  RCast (loc,r1',r2')
+	  RCast (loc,r1',k,r2')
 
   | RDynamic _ -> raw
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a0c6058576..aec4c2fa3a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -339,9 +339,9 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
 	  
-	| Cast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
+	| Cast (c1,_,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
 
-	| _, Cast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
+	| _, Cast (c2,_,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
             (isevars,base_sort_cmp pbty s1 s2)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 12559d1da7..4f956ffc6c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -48,7 +48,7 @@ let whd_castappevar_stack sigma c =
     match kind_of_term c with
       | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
 	  whrec (existential_value sigma (ev,args), l)
-      | Cast (c,_) -> whrec (c, l)
+      | Cast (c,_,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
       | _ -> s
   in 
@@ -64,11 +64,7 @@ let tj_nf_evar = Pretype_errors.tj_nf_evar
 
 let nf_evar_info evc info =
   { evar_concl = Reductionops.nf_evar evc info.evar_concl;
-    evar_hyps = List.map 
-		  (fun (id,body,typ) -> 
-		     (id,
-		      option_app (Reductionops.nf_evar evc) body,
-		      Reductionops.nf_evar evc typ)) info.evar_hyps; 
+    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
     evar_body = info.evar_body}
 
 (**********************)
@@ -107,7 +103,7 @@ let evars_to_metas sigma (emap, c) =
   let change_exist evar =
     let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
     let n = new_meta() in
-    mkCast (mkMeta n, ty) in
+    mkCast (mkMeta n, DEFAULTcast, ty) in
   let rec replace c =
     match kind_of_term c with
         Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev
@@ -163,8 +159,9 @@ let new_untyped_evar =
 
 (* All ids of sign must be distincts! *)
 let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance =
-  assert (List.length instance = named_context_length sign); 
-  if not (list_distinct (ids_of_named_context sign)) then 
+  let ctxt = named_context_of_val sign in
+  assert (List.length instance = named_context_length ctxt); 
+  if not (list_distinct (ids_of_named_context ctxt)) then 
     anomaly "new_evar_instance: two vars have the same name";
   let newev = new_untyped_evar() in
   (evar_declare sign newev typ ~src:src evd,
@@ -194,19 +191,18 @@ let make_subst env args =
 (* Converting the env into the sign of the evar to define *)
 
 let push_rel_context_to_named_context env =
-  let sign0 = named_context env in
-  let (subst,_,sign) =
+  let (subst,_,env) =
   Sign.fold_rel_context
-    (fun (na,c,t) (subst,avoid,sign) ->
+    (fun (na,c,t) (subst,avoid,env) ->
        let na = if na = Anonymous then Name(id_of_string"_") else na in
        let id = next_name_away na avoid in
        ((mkVar id)::subst,
         id::avoid,
-	add_named_decl (id,option_app (substl subst) c,
+	push_named (id,option_app (substl subst) c,
                         type_app (substl subst) t)
-	  sign))
-    (rel_context env) ~init:([],ids_of_named_context sign0,sign0)
-  in (subst, sign)
+	  env))
+    (rel_context env) ~init:([],ids_of_named_context (named_context env),env)
+  in (subst, (named_context_val env))
 
 let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ =
   let subst,sign = push_rel_context_to_named_context env in
@@ -271,7 +267,7 @@ let inverse_instance env isevars ev evi inst rhs =
              if rigid then error()
              else if
                not strict_inverse &&
-               List.exists (fun (id',_,_) -> id=id') evi.evar_hyps
+               List.exists (fun (id',_,_) -> id=id') (evar_context evi)
              then
                failwith "cannot solve pb yet"
              else t)
@@ -308,13 +304,14 @@ let do_restrict_hyps evd ev args =
   let args = Array.to_list args in
   let evi = Evd.map (evars_of !evd) ev in
   let env = evar_env evi in
-  let hyps = evi.evar_hyps in
+  let hyps = evar_context evi in
   let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
   (* No care is taken in case the evar type uses vars filtered out!
      Is it important ? *)
   let nc =
-    e_new_evar evd (reset_with_named_context sign env)
-      ~src:(evar_source ev !evd) evi.evar_concl in
+    let env =
+      Sign.fold_named_context push_named sign ~init:(reset_context env) in
+    e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in
   evd := Evd.evar_define ev nc !evd;
   let (evn,_) = destEvar nc in
   mkEvar(evn,Array.of_list ncargs)
@@ -351,7 +348,8 @@ let real_clean env isevars ev evi args rhs =
           (try List.assoc t subst
            with Not_found ->
              if
-               not rigid or List.exists (fun (id',_,_) -> id=id') evi.evar_hyps
+               not rigid 
+		 or List.exists (fun (id',_,_) -> id=id') (evar_context evi)
              then t
              else
                error_not_clean env (evars_of !evd) ev rhs
@@ -430,7 +428,7 @@ let head_is_evar isevars =
   let rec hrec k = match kind_of_term k with
     | Evar n   -> not (Evd.is_defined_evar isevars n)
     | App (f,_) -> hrec f
-    | Cast (c,_) -> hrec c
+    | Cast (c,_,_) -> hrec c
     | _ -> false
   in 
   hrec 
@@ -438,7 +436,7 @@ let head_is_evar isevars =
 let rec is_eliminator c = match kind_of_term c with
   | App _    -> true
   | Case _ -> true
-  | Cast (c,_) -> is_eliminator c
+  | Cast (c,_,_) -> is_eliminator c
   | _ -> false
 
 let head_is_embedded_evar isevars c =
@@ -449,7 +447,7 @@ let head_evar =
     | Evar (ev,_)       -> ev
     | Case (_,_,c,_) -> hrec c
     | App (c,_)        -> hrec c
-    | Cast (c,_)        -> hrec c
+    | Cast (c,_,_)        -> hrec c
     | _                   -> failwith "headconstant"
   in 
   hrec 
@@ -494,7 +492,7 @@ let status_changed lev (pbty,t1,t2) =
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   if argsv1 = argsv2 then (isevars,[]) else
   let evd = Evd.map (evars_of isevars) ev in
-  let hyps = evd.evar_hyps in
+  let hyps = evar_context evd in
   let (isevars',_,rsign) = 
     array_fold_left2
       (fun (isevars,sgn,rsgn) a1 a2 ->
@@ -507,8 +505,9 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   in
   let nsign = List.rev rsign in
   let (evd',newev) =
-    new_evar isevars (reset_with_named_context nsign env)
-      ~src:(evar_source ev isevars) evd.evar_concl in
+    let env =
+      Sign.fold_named_context push_named nsign ~init:(reset_context env) in
+    new_evar isevars env ~src:(evar_source ev isevars) evd.evar_concl in
   let evd'' = Evd.evar_define ev newev evd' in
   evd'', [ev]
 
@@ -585,7 +584,8 @@ let define_evar_as_arrow evd (ev,args) =
   let evenv = evar_env evi in
   let (evd1,dom) = new_evar evd evenv (new_Type()) in
   let nvar =
-    next_ident_away (id_of_string "x") (ids_of_named_context evi.evar_hyps) in
+    next_ident_away (id_of_string "x")
+      (ids_of_named_context (evar_context evi)) in
   let newenv = push_named (nvar, None, dom) evenv in
   let (evd2,rng) =
     new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index b3e5a4dd9f..e6bdcbd9bb 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -43,8 +43,8 @@ val e_new_evar :
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context -> evar_defs -> types -> ?src:loc * hole_kind -> constr list ->
- evar_defs * constr
+ named_context_val -> evar_defs -> types -> ?src:loc * hole_kind ->
+   constr list -> evar_defs * constr
 
 (***********************************************************)
 (* Instanciate evars *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 35012f6bd6..c58d921ebc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -29,9 +29,11 @@ type evar_body =
 
 type evar_info = {
   evar_concl : constr;
-  evar_hyps : named_context;
+  evar_hyps : named_context_val;
   evar_body : evar_body}
 
+let evar_context evi = named_context_of_val evi.evar_hyps
+
 module Evarmap = Intmap
 
 type evar_map1 = evar_info Evarmap.t
@@ -107,14 +109,14 @@ let existential_type sigma (n,args) =
     try map sigma n
     with Not_found ->
       anomaly ("Evar "^(string_of_existential n)^" was not declared") in
-  let hyps = info.evar_hyps in
+  let hyps = evar_context info in
   instantiate_evar hyps info.evar_concl (Array.to_list args)
 
 exception NotInstantiatedEvar
 
 let existential_value sigma (n,args) =
   let info = map sigma n in
-  let hyps = info.evar_hyps in
+  let hyps = evar_context info in
   match evar_body info with
     | Evar_defined c ->
 	instantiate_evar hyps c (Array.to_list args)
@@ -519,7 +521,7 @@ let pr_meta_map mmap =
 let pr_idl idl = prlist_with_sep pr_spc pr_id idl
 
 let pr_evar_info evi =
-  let phyps = pr_idl (List.rev (ids_of_named_context evi.evar_hyps)) in
+  let phyps = pr_idl (List.rev (ids_of_named_context (evar_context evi))) in
   let pty = print_constr evi.evar_concl in
   let pb =
     match evi.evar_body with
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 9dd0c33fb4..506ce44877 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -31,9 +31,10 @@ type evar_body =
 
 type evar_info = {
   evar_concl : constr;
-  evar_hyps : named_context;
+  evar_hyps : Environ.named_context_val;
   evar_body : evar_body}
 
+val evar_context : evar_info -> named_context
 type evar_map
 
 val empty : evar_map
@@ -125,7 +126,7 @@ type hole_kind =
 val is_defined_evar :  evar_defs -> existential -> bool
 val is_undefined_evar :  evar_defs -> constr -> bool
 val evar_declare :
-  named_context -> evar -> types -> ?src:loc * hole_kind ->
+  Environ.named_context_val -> evar -> types -> ?src:loc * hole_kind ->
   evar_defs -> evar_defs
 val evar_define : evar -> constr -> evar_defs -> evar_defs
 val evar_source : existential_key -> evar_defs -> loc * hole_kind
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8cd3dc2c4a..0325a3acd6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -447,7 +447,7 @@ let make_case_gen env   = make_case_com None env
 
 let change_sort_arity sort = 
   let rec drec a = match kind_of_term a with
-    | Cast (c,t) -> drec c 
+    | Cast (c,_,_) -> drec c 
     | Prod (n,t,c) -> mkProd (n, t, drec c)
     | LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c)
     | Sort _ -> mkSort sort
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d0dca036e3..813a6a2699 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -363,7 +363,7 @@ let control_only_guard env =
     | Case(_,p,c,b) -> control_rec p;control_rec c;Array.iter control_rec b
     | Evar (_,cl)        -> Array.iter control_rec cl
     | App (c,cl)         -> control_rec c; Array.iter control_rec cl
-    | Cast (c1,c2)       -> control_rec c1; control_rec c2
+    | Cast (c1,_, c2)  -> control_rec c1; control_rec c2
     | Prod (_,c1,c2)     -> control_rec c1; control_rec c2
     | Lambda (_,c1,c2)   -> control_rec c1; control_rec c2
     | LetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 34eb6d78de..64b63548d4 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -179,15 +179,15 @@ let special_meta = (-1)
 (* Tries to match a subterm of [c] with [pat] *)
 let rec sub_match nocc pat c =
   match kind_of_term c with
-  | Cast (c1,c2) ->
+  | Cast (c1,k,c2) ->
     (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1] in
-      (lm,mkCast (List.hd lc, c2))
+      (lm,mkCast (List.hd lc, k,c2))
     | NextOccurrence nocc ->
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
-      (lm,mkCast (List.hd lc, c2)))
-  | Lambda (x,c1,c2) ->
+      (lm,mkCast (List.hd lc, k,c2)))
+ | Lambda (x,c1,c2) ->
     (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;c2] in
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index c67917477d..df9139db1f 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -99,7 +99,7 @@ let rec pattern_of_constr t =
     | Var id -> PVar id
     | Sort (Prop c) -> PSort (RProp c)
     | Sort (Type _) -> PSort (RType None)
-    | Cast (c,_)      -> pattern_of_constr c
+    | Cast (c,_,_)      -> pattern_of_constr c
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
@@ -213,7 +213,7 @@ let rec pat_of_raw metas vars = function
       PSort s
   | RHole _ ->
       PMeta None
-  | RCast (_,c,t) ->
+  | RCast (_,c,_,t) ->
       Options.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index d3a602ac28..f1f95695d3 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -53,7 +53,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=type_app (nf_evar sigma) v;utj_type=t}
 
 let env_ise sigma env =
-  let sign = named_context env in
+  let sign = named_context_val env in
   let ctxt = rel_context env in
   let env0 = reset_with_named_context sign env in
   Sign.fold_rel_context
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 148be3991d..c0e20c399e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -262,7 +262,7 @@ let rec pretype tycon env isevars lvar = function
   | REvar (loc, ev, instopt) ->
       (* Ne faudrait-il pas s'assurer que hyps est bien un
       sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-      let hyps = (Evd.map (evars_of !isevars) ev).evar_hyps in
+      let hyps = evar_context (Evd.map (evars_of !isevars) ev) in
       let args = match instopt with
         | None -> instance_from_named_context hyps
         | Some inst -> failwith "Evar subtitutions not implemented" in
@@ -637,7 +637,7 @@ let rec pretype tycon env isevars lvar = function
 	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
                         buildrec new_ids (pat::patlist) new_avoid (n-1) b
                           
-	            | RCast (_,c,_) ->    (* Oui, il y a parfois des cast *)
+	            | RCast (_,c,_,_) ->    (* Oui, il y a parfois des cast *)
 	                buildrec ids patlist avoid n c
                         
 	            | _ -> (* eta-expansion *)
@@ -873,7 +873,7 @@ let rec pretype tycon env isevars lvar = function
 	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
                         buildrec new_ids (pat::patlist) new_avoid (n-1) b
                           
-	            | RCast (_,c,_) ->    (* Oui, il y a parfois des cast *)
+	            | RCast (_,c,_,_) ->    (* Oui, il y a parfois des cast *)
 	                buildrec ids patlist avoid n c
                         
 	            | _ -> (* eta-expansion *)
@@ -906,12 +906,12 @@ let rec pretype tycon env isevars lvar = function
 	((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	tycon env (* loc *) (po,tml,eqns)
 
-  | RCast(loc,c,t) ->
+  | RCast(loc,c,k,t) ->
       let tj = pretype_type empty_tycon env isevars lvar t in
       let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
       (* User Casts are for helping pretyping, experimentally not to be kept*)
       (* ... except for Correctness *)
-      let v = mkCast (cj.uj_val, tj.utj_val) in
+      let v = mkCast (cj.uj_val, k, tj.utj_val) in
       let cj = { uj_val = v; uj_type = tj.utj_val } in
       inh_conv_coerce_to_tycon loc env isevars cj tycon
 
@@ -1006,7 +1006,8 @@ let ise_infer_gen fail_evar sigma env lvar exptyp c =
   let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
   let isevars = ref (create_evar_defs sigma) in
   let j = unsafe_infer tycon isevars env lvar c in
-  if fail_evar then check_evars env sigma isevars (mkCast(j.uj_val,j.uj_type));
+  if fail_evar then 
+    check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
   (!isevars, j)
 
 let ise_infer_type_gen fail_evar sigma env lvar c =
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index b915313951..dde8490d05 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -70,7 +70,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * rawconstr
+  | RCast of loc * rawconstr * cast_kind * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
@@ -110,7 +110,7 @@ let map_rawconstr f = function
   | RRec (loc,fk,idl,bl,tyl,bv) ->
       RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
             Array.map f tyl,Array.map f bv)
-  | RCast (loc,c,t) -> RCast (loc,f c,f t)
+  | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
   
 
@@ -184,7 +184,7 @@ let occur_rawconstr id =
                 (na=Name id or not(occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
-    | RCast (loc,c,t) -> (occur c) or (occur t)
+    | RCast (loc,c,_,t) -> (occur c) or (occur t)
     | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
@@ -211,7 +211,7 @@ let loc_of_rawconstr = function
   | RRec (loc,_,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
-  | RCast (loc,_,_) -> loc
+  | RCast (loc,_,_,_) -> loc
   | RDynamic (loc,_) -> loc
 
 type 'a raw_red_flag = {
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index b56e862ac6..4e4df6b39c 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -67,7 +67,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * Evd.hole_kind)
-  | RCast of loc * rawconstr * rawconstr
+  | RCast of loc * rawconstr * cast_kind * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 67c0fc8561..c9ab57d02c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -47,7 +47,7 @@ type local_state_reduction_function = state -> state
 let rec whd_state (x, stack as s) =
   match kind_of_term x with
     | App (f,cl) -> whd_state (f, append_stack cl stack)
-    | Cast (c,_)  -> whd_state (c, stack)
+    | Cast (c,_,_)  -> whd_state (c, stack)
     | _             -> s
 
 let appterm_of_stack (f,s) = (f,list_of_stack s)
@@ -254,7 +254,7 @@ let rec whd_state_gen flags env sigma =
 	     | Some  body -> whrec (body, stack)
 	     | None -> s)
       | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
-      | Cast (c,_) -> whrec (c, stack)
+      | Cast (c,_,_) -> whrec (c, stack)
       | App (f,cl)  -> whrec (f, append_stack cl stack)
       | Lambda (na,t,c) ->
           (match decomp_stack stack with
@@ -299,7 +299,7 @@ let local_whd_state_gen flags =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
       | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
-      | Cast (c,_) -> whrec (c, stack)
+      | Cast (c,_,_) -> whrec (c, stack)
       | App (f,cl)  -> whrec (f, append_stack cl stack)
       | Lambda (_,_,c) ->
           (match decomp_stack stack with
@@ -338,6 +338,47 @@ let local_whd_state_gen flags =
   in 
   whrec
 
+let rec whd_betaiotaevar_preserving_vm_cast env sigma t = 
+  let rec stacklam_var subst t stack =
+    match (decomp_stack stack,kind_of_term t) with
+    | Some (h,stacktl), Lambda (_,_,c) ->
+	begin match kind_of_term h with
+	| Rel i when not (evaluable_rel i env) ->
+	    stacklam_var (h::subst) c stacktl
+        | Var id when  not (evaluable_named id env)->
+	    stacklam_var (h::subst) c stacktl
+	| _ -> whrec (substl subst t, stack)
+	end
+    | _ -> whrec (substl subst t, stack)
+  and whrec (x, stack as s) =
+    match kind_of_term x with
+      | Evar ev ->
+	  (match existential_opt_value sigma ev with
+	     | Some body -> whrec (body, stack)
+	     | None -> s)
+      | Cast (c,VMcast,t) ->
+	  let c = app_stack (whrec (c,empty_stack)) in
+	  let t = app_stack (whrec (t,empty_stack)) in
+	  (mkCast(c,VMcast,t),stack)
+      | Cast (c,DEFAULTcast,_) ->
+	  whrec (c, stack)
+      | App (f,cl)  -> whrec (f, append_stack cl stack)
+      | Lambda (na,t,c) ->
+          (match decomp_stack stack with
+           | Some (a,m) -> stacklam_var [a] c m
+           | _ -> s)
+      | Case (ci,p,d,lf) ->
+          let (c,cargs) = whrec (d, empty_stack) in
+          if reducible_mind_case c then
+            whrec (reduce_mind_case
+                     {mP=p; mconstr=c; mcargs=list_of_stack cargs;
+		      mci=ci; mlf=lf}, stack)
+          else 
+	    (mkCase (ci, p, app_stack (c,cargs), lf), stack)
+      | x -> s
+  in 
+  app_stack (whrec (t,empty_stack))
+
 (* 1. Beta Reduction Functions *)
 
 let whd_beta_state = local_whd_state_gen beta
@@ -512,22 +553,22 @@ let plain_instance s c =
   let rec irec u = match kind_of_term u with
     | Meta p -> (try List.assoc p s with Not_found -> u)
     | App (f,l) when isCast f ->
-        let (f,t) = destCast f in
+        let (f,_,t) = destCast f in
         let l' = Array.map irec l in 
         (match kind_of_term f with
-          | Meta p ->
-              (* Don't flatten application nodes: this is used to extract a
-                 proof-term from a proof-tree and we want to keep the structure
-                 of the proof-tree *)
-              (try let g = List.assoc p s in
-              match kind_of_term g with
-                | App _ -> 
-                    let h = id_of_string "H" in
-                    mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
-                | _ -> mkApp (g,l')
-              with Not_found -> mkApp (f,l'))
-          | _ -> mkApp (irec f,l'))
-    | Cast (m,_) when isMeta m ->
+        | Meta p ->
+	    (* Don't flatten application nodes: this is used to extract a
+               proof-term from a proof-tree and we want to keep the structure
+               of the proof-tree *)
+	    (try let g = List.assoc p s in
+	    match kind_of_term g with
+            | App _ -> 
+                let h = id_of_string "H" in
+                mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
+            | _ -> mkApp (g,l')
+	    with Not_found -> mkApp (f,l'))
+        | _ -> mkApp (irec f,l'))	
+    | Cast (m,_,_) when isMeta m ->
 	(try List.assoc (destMeta m) s with Not_found -> u)
     | _ -> map_constr irec u
   in 
@@ -598,7 +639,7 @@ let splay_prod_assum env sigma =
     | LetIn (x,b,t,c) ->
 	prodec_rec (push_rel (x, Some b, t) env)
 	  (Sign.add_rel_decl (x, Some b, t) l) c
-    | Cast (c,_)    -> prodec_rec env l c
+    | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> l,t
   in
   prodec_rec env Sign.empty_rel_context
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 29a28f0f74..42a53224a6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -111,6 +111,10 @@ val whd_betadeltaiotaeta_stack :  stack_reduction_function
 val whd_betadeltaiotaeta_state :  state_reduction_function
 val whd_betadeltaiotaeta :  reduction_function
 
+val whd_betaiotaevar_preserving_vm_cast : reduction_function
+
+
+
 val beta_applist : constr * constr list -> constr
 
 val hnf_prod_app     : env ->  evar_map -> constr -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a75e48a8e9..715f54731c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -81,12 +81,12 @@ let typeur sigma metamap =
     | App(f,args)->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
-    | Cast (c,t) -> t
+    | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
   and sort_of env t = 
     match kind_of_term t with
-    | Cast (c,s) when isSort s -> destSort s
+    | Cast (c,_, s) when isSort s -> destSort s
     | Sort (Prop c) -> type_0
     | Sort (Type u) -> Type (Univ.super u)
     | Prod (name,t,c2) ->
@@ -104,7 +104,7 @@ let typeur sigma metamap =
 
   and sort_family_of env t =
     match kind_of_term t with
-    | Cast (c,s) when isSort s -> family_of_sort (destSort s)
+    | Cast (c,_, s) when isSort s -> family_of_sort (destSort s)
     | Sort (Prop c) -> InType
     | Sort (Type u) -> InType
     | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c9189ad2f1..ef0867f7c4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -440,7 +440,7 @@ let rec red_elim_const env sigma ref largs =
 and construct_const env sigma = 
   let rec hnfstack (x, stack as s) =
     match kind_of_term x with
-      | Cast (c,_) -> hnfstack (c, stack)
+      | Cast (c,_,_) -> hnfstack (c, stack)
       | App (f,cl) -> hnfstack (f, append_stack cl stack)
       | Lambda (id,t,c) ->
           (match decomp_stack stack with 
@@ -494,7 +494,7 @@ let try_red_product env sigma c =
                         let stack' = stack_assign stack recargnum recarg' in
                         simpfun (app_stack (f,stack')))
              | _ -> simpfun (appvect (redrec env f, l)))
-      | Cast (c,_) -> redrec env c
+      | Cast (c,_,_) -> redrec env c
       | Prod (x,a,b) -> mkProd (x, a, redrec (push_rel (x,None,a) env) b)
       | LetIn (x,a,b,t) -> redrec env (subst1 a t)
       | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf))
@@ -522,7 +522,7 @@ let hnf_constr env sigma c =
 		 stacklam redrec [a] c rest)
       | LetIn (n,b,t,c) -> stacklam redrec [b] c largs
       | App (f,cl)   -> redrec (f, append_stack cl largs)
-      | Cast (c,_) -> redrec (c, largs)
+      | Cast (c,_,_) -> redrec (c, largs)
       | Case (ci,p,c,lf) ->
           (try
              redrec 
@@ -563,7 +563,7 @@ let whd_nf env sigma c =
 		 stacklam nf_app [a1] c2 rest)
       | LetIn (n,b,t,c) -> stacklam nf_app [b] c stack
       | App (f,cl) -> nf_app (f, append_stack cl stack)
-      | Cast (c,_) -> nf_app (c, stack)
+      | Cast (c,_,_) -> nf_app (c, stack)
       | Case (ci,p,d,lf) ->
           (try
              nf_app (special_red_case sigma env nf_app (ci,p,d,lf), stack)
@@ -705,13 +705,13 @@ let rec substlin env name n ol c =
 	              let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf)
                       in (n3,ol3,mkCase (ci, p', d', Array.of_list lf'))))
         
-    | Cast (c1,c2)   ->
+    | Cast (c1,k,c2)   ->
         let (n1,ol1,c1') = substlin env name n ol c1 in
         (match ol1 with 
-           | [] -> (n1,[],mkCast (c1',c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkCast (c1',c2')))
+           | [] -> (n1,[],mkCast (c1',k,c2))
+           | _  -> 
+	       let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
+               (n2,ol2,mkCast (c1',k,c2')))
 
     | Fix _ -> 
         (warning "do not consider occurrences inside fixpoints"; (n,ol,c))
@@ -815,7 +815,7 @@ let one_step_reduce env sigma c =
 	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with
              | Reduced s' -> s'
 	     | NotReducible -> raise NotStepReducible)
-      | Cast (c,_) -> redrec (c,largs)
+      | Cast (c,_,_) -> redrec (c,largs)
       | _ when isEvalRef env x ->
 	  let ref =
             try destEvalRef x
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 1a6521d985..6db5d428ad 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -42,7 +42,7 @@ let rec pr_constr c = match kind_of_term c with
   | Meta n -> str "Meta(" ++ int n ++ str ")"
   | Var id -> pr_id id
   | Sort s -> print_sort s
-  | Cast (c,t) -> hov 1 
+  | Cast (c,_, t) -> hov 1 
       (str"(" ++ pr_constr c ++ cut() ++
        str":" ++ pr_constr t ++ str")")
   | Prod (Name(id),t,c) -> hov 1
@@ -120,7 +120,8 @@ let pr_rel_decl env (na,c,typ) =
 
 let print_named_context env =
   hv 0 (fold_named_context
-	  (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+	  (fun env d pps -> 
+	    pps ++ ws 2 ++ pr_var_decl env d)
           env ~init:(mt ()))
 
 let print_rel_context env = 
@@ -132,7 +133,8 @@ let print_env env =
   let sign_env =
     fold_named_context
       (fun env d pps ->
-         let pidt =  pr_var_decl env d in (pps ++ fnl () ++ pidt))
+         let pidt =  pr_var_decl env d in
+	 (pps ++ fnl () ++ pidt))
       env ~init:(mt ()) 
   in
   let db_env =
@@ -262,11 +264,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
 
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
@@ -278,7 +280,7 @@ let rec strip_head_cast c = match kind_of_term c with
 let map_constr_with_named_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 na l) c)
   | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
   | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
@@ -313,7 +315,7 @@ let fold_rec_types g (lna,typarray,_) e =
 let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
-  | Cast (c,t) -> let c' = f l c in mkCast (c', f l t)
+  | Cast (c,k,t) -> let c' = f l c in mkCast (c',k,f l t)
   | Prod (na,t,c) ->
       let t' = f l t in
       mkProd (na, t', f (g (na,None,t) l) c)
@@ -348,10 +350,10 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
 let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> cstr
-  | Cast (c,t) -> 
+  | Cast (c,k, t) -> 
       let c' = f l c in
       let t' = f l t in
-      if c==c' && t==t' then cstr else mkCast (c', t')
+      if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
       let c' = f (g (na,None,t) l) c in
@@ -405,7 +407,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
 let fold_constr_with_binders g f n acc c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
-  | Cast (c,t) -> f n (f n acc c) t
+  | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (_,t,c) -> f (g n) (f n acc t) c
   | Lambda (_,t,c) -> f (g n) (f n acc t) c
   | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
@@ -429,7 +431,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
 let iter_constr_with_full_binders g f l c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
-  | Cast (c,t) -> f l c; f l t
+  | Cast (c,_, t) -> f l c; f l t
   | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
   | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
   | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
@@ -695,7 +697,7 @@ let hdchar env c =
     | Prod (_,_,c)       -> hdrec (k+1) c
     | Lambda (_,_,c)     -> hdrec (k+1) c
     | LetIn (_,_,_,c)    -> hdrec (k+1) c
-    | Cast (c,_)         -> hdrec k c
+    | Cast (c,_,_)         -> hdrec k c
     | App (f,l)         -> hdrec k f
     | Const kn       ->
 	let c = lowercase_first_char (id_of_label (con_label kn)) in
@@ -786,6 +788,7 @@ let ids_of_rel_context sign =
   Sign.fold_rel_context
     (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
     sign ~init:[]
+
 let ids_of_named_context sign =
   Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
 
@@ -793,6 +796,7 @@ let ids_of_context env =
   (ids_of_rel_context (rel_context env))
   @ (ids_of_named_context (named_context env))
 
+
 let names_of_rel_context env =
   List.map (fun (na,_,_) -> na) (rel_context env)
 
@@ -824,7 +828,7 @@ let is_global id =
     false
 
 let is_section_variable id =
-  try let _ = Sign.lookup_named id (Global.named_context()) in true
+  try let _ = Global.lookup_named id in true
   with Not_found -> false
 
 let next_global_ident_from allow_secvar id avoid = 
@@ -934,7 +938,7 @@ let eta_eq_constr =
 
 (* iterator on rel context *)
 let process_rel_context f env =
-  let sign = named_context env in
+  let sign = named_context_val env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
   Sign.fold_rel_context f rels ~init:env0
@@ -1006,6 +1010,6 @@ let rec rename_bound_var env l c =
   | Prod (Anonymous,c1,c2) ->
         let env' = push_rel (Anonymous,None,c1) env in
         mkProd (Anonymous, c1, rename_bound_var env' l c2)
-  | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
+  | Cast (c,k,t) -> mkCast (rename_bound_var env l c, k,t)
   | x -> c
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index dd2d781d54..38febedaa5 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -112,16 +112,16 @@ let rec execute env evd cstr =
         let j1 = execute env evd c1 in
         let j2 = execute env evd c2 in
         let j2 = type_judgment env j2 in
-        let _ =  judge_of_cast env j1 j2 in
+        let _ =  judge_of_cast env j1 DEFAULTcast j2 in
         let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
         let j3 = execute env1 evd c3 in
         judge_of_letin env name j1 j2 j3
   
-    | Cast (c,t) ->
+    | Cast (c,k,t) ->
         let cj = execute env evd c in
         let tj = execute env evd t in
 	let tj = type_judgment env tj in
-        let j, _ = judge_of_cast env cj tj in
+        let j, _ = judge_of_cast env cj k tj in
 	j
 
 and execute_recdef env evd (names,lar,vdef) =