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, 77 insertions, 65 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index 71545d966..a3e1902c0 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -131,7 +131,7 @@ let rec make_prb gls additionnal_terms =
 		      add_disequality state (HeqnH (idp,id)) ph nh) 
 		   !pos_hyps;
 		 neg_hyps:=(id,nh):: !neg_hyps
-	 end) gls.it.evar_hyps;
+	 end) (Environ.named_context_of_val gls.it.evar_hyps);
     begin
       match atom_of_constr env gls.it.evar_concl with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6bc667339..41619c85f 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -354,7 +354,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let rec names_prod t = match kind_of_term t with 
 	  | Prod(n,_,t) -> n::(names_prod t)
 	  | LetIn(_,_,_,t) -> names_prod t
-	  | Cast(t,_) -> names_prod t
+	  | Cast(t,_,_) -> names_prod t
 	  | _ -> []
 	in 
 	let field_names = 
@@ -515,7 +515,7 @@ let rec extract_term env mle mlt c args =
  	extract_app env mle mlt (extract_fix env mle i recd) args 
     | CoFix (i,recd) ->
  	extract_app env mle mlt (extract_fix env mle i recd) args
-    | Cast (c, _) -> extract_term env mle mlt c args
+    | Cast (c,_,_) -> extract_term env mle mlt c args
     | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false 
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 657d4cba5..fb75655f0 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -91,8 +91,8 @@ let compare_constr_int f t1 t2 =
     | Meta m1, Meta m2 -> m1 - m2
     | Var id1, Var id2 -> Pervasives.compare id1 id2
     | Sort s1, Sort s2 -> Pervasives.compare 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) 
     | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
 	(f =? f) t1 t2 c1 c2 
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index a1e620a23..41a100c2b 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -59,8 +59,8 @@ let unif t1 t2=
 		if Intset.is_empty (free_rels t) && 
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
-	  | Cast(_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
- 	  | _,Cast(_,_)->Queue.add (nt1,strip_outer_cast nt2) bige 
+	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
+ 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige 
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
 	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 5e31d5675..e40cd2676 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -85,13 +85,13 @@ let string_of_R_constant kn =
 
 let rec string_of_R_constr c =
  match kind_of_term c with
-   Cast (c,t) -> string_of_R_constr c
+   Cast (c,_,_) -> string_of_R_constr c
   |Const c -> string_of_R_constant c
   | _ -> "not_of_constant"
 
 let rec rational_of_constr c =
   match kind_of_term c with
-  | Cast (c,t) -> (rational_of_constr c)
+  | Cast (c,_,_) -> (rational_of_constr c)
   | App (c,args) ->
       (match (string_of_R_constr c) with
 	 | "Ropp" -> 
@@ -122,7 +122,7 @@ let rec rational_of_constr c =
 let rec flin_of_constr c =
   try(
     match kind_of_term c with
-  | Cast (c,t) -> (flin_of_constr c)
+  | Cast (c,_,_) -> (flin_of_constr c)
   | App (c,args) ->
       (match (string_of_R_constr c) with
 	   "Ropp" -> 
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 27f14aedf..064f279f0 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -74,7 +74,7 @@ let  rec mkevarmap_from_listex lex =
 		  let _ = prconstr typ in*)
 		  let info ={
 			 evar_concl = typ;
-			 evar_hyps = empty_named_context;
+			 evar_hyps = empty_named_context_val;
 			 evar_body = Evar_empty} in
 		  Evd.add (mkevarmap_from_listex lex') ex info
 
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 09b918be5..807883115 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -93,7 +93,7 @@ let rec def_const_in_term_rec vl x =
           def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
    | Case(_,x,t,a) 
         -> def_const_in_term_rec vl x
-   | Cast(x,t)-> def_const_in_term_rec vl t
+   | Cast(x,_,t)-> def_const_in_term_rec vl t
    | Const(c)  -> def_const_in_term_rec vl (lookup_constant c vl).const_type
    | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
 ;;
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 532955661..f8328f21d 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -106,7 +106,7 @@ let make_final_cmd f optname clear_names constr path =
     add_clear_names_if_necessary (f optname constr path) clear_names;;
 
 let (rem_cast:pbp_rule) = function
-    (a,c,cf,o, Cast(f,_), p, func) ->
+    (a,c,cf,o, Cast(f,_,_), p, func) ->
       Some(func a c cf o (kind_of_term f) p)
   | _ -> None;;
 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 2560b0b82..1c89156b5 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -54,7 +54,7 @@ and ngoal=
      {newhyp : nhyp list;
       t_concl : Term.constr;
       t_full_concl: Term.constr;
-      t_full_env: Sign.named_context}
+      t_full_env: Environ.named_context_val}
 and ntree=
       {t_info:string;
 	t_goal:ngoal;
@@ -151,7 +151,7 @@ let seq_to_lnhyp sign sign' cl =
       {newhyp=nh;
        t_concl=cl;
        t_full_concl=long_type_hyp !lh cl;
-       t_full_env = sign@sign'}
+       t_full_env = Environ.val_of_named_context (sign@sign')}
 ;;
 
 
@@ -247,6 +247,7 @@ let old_sign osign sign =
 let  to_nproof sigma osign pf =
   let rec to_nproof_rec sigma osign pf =
     let {evar_hyps=sign;evar_concl=cl} = pf.goal in
+    let sign = Environ.named_context_of_val sign in
     let nsign = new_sign osign sign in 
     let oldsign = old_sign osign sign in 
     match pf.ref with
@@ -759,7 +760,7 @@ let rec nsortrec vl x =
           nsortrec vl (mkInd (inductive_of_constructor c))
    | Case(_,x,t,a) 
         -> nsortrec vl x
-   | Cast(x,t)-> nsortrec vl t
+   | Cast(x,_, t)-> nsortrec vl t
    | Const c  -> nsortrec vl (lookup_constant c vl).const_type
    | _ -> nsortrec vl (type_of vl Evd.empty x)
 ;;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 391cc0f7c..69c6674d3 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -411,7 +411,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CDynamic (_, _) -> assert false
    | CDelimiters (_, key, num) -> 
 	 CT_num_encapsulator(CT_num_type key , xlate_formula  num)
-   | CCast (_, e, t) -> 
+   | CCast (_, e,_, t) -> 
        CT_coerce_TYPED_FORMULA_to_FORMULA
 	 (CT_typed_formula(xlate_formula e, xlate_formula t))
    | CPatVar (_, (_,i)) when is_int_meta i ->
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 30562cd44..46b987112 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -460,7 +460,7 @@ type constr_path =
 let context operation path (t : constr) =
   let rec loop i p0 t = 
     match (p0,kind_of_term t) with 
-      | (p, Cast (c,t)) -> mkCast (loop i p c,t)
+      | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t)
       | ([], _) -> operation i t
       | ((P_APP n :: p),  App (f,v)) ->
 	  let v' = Array.copy v in
@@ -498,7 +498,7 @@ let context operation path (t : constr) =
 
 let occurence path (t : constr) =
   let rec loop p0 t = match (p0,kind_of_term t) with
-    | (p, Cast (c,t)) -> loop p c
+    | (p, Cast (c,_,_)) -> loop p c
     | ([], _) -> t
     | ((P_APP n :: p),  App (f,v)) -> loop p v.(pred n)
     | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n)
@@ -524,7 +524,7 @@ let abstract_path typ path t =
 
 let focused_simpl path gl =
   let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
-  convert_concl_no_check newc gl
+  convert_concl_no_check newc DEFAULTcast gl
 
 let focused_simpl path = simpl_time (focused_simpl path)
 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index aa7766785..4121580ff 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -132,7 +132,7 @@ let rec (find_call_occs:
   | Meta(_) -> error "find_call_occs : Meta"
   | Evar(_) -> error "find_call_occs : Evar"
   | Sort(_)  -> error "find_call_occs : Sort"
-  | Cast(_,_) -> error "find_call_occs : cast"
+  | Cast(_,_,_) -> error "find_call_occs : cast"
   | Prod(_,_,_) -> error "find_call_occs : Prod"
   | Lambda(_,_,_) -> error "find_call_occs : Lambda"
   | LetIn(_,_,_,_) -> error "find_call_occs : let in"
@@ -514,7 +514,7 @@ let com_terminate fonctional_ref input_type relation_ast wf_thm_ast
   let (proofs_constr:constr list) =
       List.map (fun x -> interp_constr evmap env x) proofs in
     (start_proof thm_name
-       (IsGlobal (Proof Lemma)) (Environ.named_context env) (hyp_terminates fonctional_ref)
+       (IsGlobal (Proof Lemma)) (Environ.named_context_val env) (hyp_terminates fonctional_ref)
        (fun _ _ -> ());
      by (whole_start fonctional_ref
 	   input_type relation wf_thm proofs_constr);
@@ -713,7 +713,7 @@ let (com_eqn : identifier ->
     let eq_constr = interp_constr evmap env eq in
     let f_constr = (constr_of_reference f_ref) in
       (start_proof eq_name (IsGlobal (Proof Lemma))
-       (Environ.named_context env) eq_constr (fun _ _ -> ());
+       (Environ.named_context_val env) eq_constr (fun _ _ -> ());
        by
 	 (start_equation f_ref terminate_ref
 	    (fun x ->
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index fb0e66526..3b937c7a6 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -212,7 +212,7 @@ let compute_rhs bodyi index_of_f =
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
           PApp (pattern_of_constr f, Array.map aux args)
-      | Cast (c,t) -> aux c 
+      | Cast (c,_,_) -> aux c 
       | _ -> pattern_of_constr c
   in
   aux bodyi
@@ -297,7 +297,7 @@ binary search trees (see file \texttt{Quote.v}) *)
 let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
-     | Cast(c,_) -> closed_under cset c  
+     | Cast(c,_,_) -> closed_under cset c  
      | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
      | _ -> false)
     
@@ -360,7 +360,7 @@ let rec subterm gl (t : constr) (t' : constr) =
   (pf_conv_x gl t t') or
   (match (kind_of_term t) with 
      | App (f,args) -> array_exists (fun t -> subterm gl t t') args
-     | Cast(t,_) -> (subterm gl t t')
+     | Cast(t,_,_) -> (subterm gl t t')
      | _ -> false)
            
 (*s We want to sort the list according to reverse subterm order. *)
@@ -447,8 +447,8 @@ let quote f lid gl =
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl
+    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
+    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
 
 (*i 
 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index d3068c862..4884f23c6 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -773,7 +773,7 @@ open RedFlags
 let polynom_unfold_tac =
   let flags =
     (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
-  reduct_in_concl (cbv_norm_flags flags)
+  reduct_in_concl (cbv_norm_flags flags,DEFAULTcast)
       
 let polynom_unfold_tac_in_term gl =
   let flags = 
diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v
index d1cb80275..342c03dba 100644
--- a/contrib/rtauto/Rtauto.v
+++ b/contrib/rtauto/Rtauto.v
@@ -18,7 +18,7 @@ Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 Ltac clean:=try (simpl;congruence).
 
 Inductive form:Set:=
-Atom : positive -> form
+  Atom : positive -> form
 | Arrow : form -> form -> form
 | Bot
 | Conjunct : form -> form -> form 
@@ -395,4 +395,4 @@ exact (Reflect (empty \ A \ B \ C)
   (I_Or_r (I_And (Ax 2) (Ax 4))))))).
 Qed.
 Print toto.
-*)
\ No newline at end of file
+*)
diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml
index 0865a825c..801122476 100644
--- a/contrib/rtauto/refl_tauto.ml
+++ b/contrib/rtauto/refl_tauto.ml
@@ -113,7 +113,7 @@ let rec make_form atom_env gls term =
 	      Arrow (fa,fb)
 	  else
 	    make_atom atom_env (normalize term)
-      | Cast(a,b) -> 
+      | Cast(a,_,_) -> 
 	  make_form atom_env gls a
       | Ind ind ->
 	  if ind = Lazy.force li_False then
@@ -273,7 +273,8 @@ let rtauto_tac gls=
       (pf_env gls) (Tacmach.project gls) gl <> InProp 
     then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
-  let hyps=make_hyps gamma gls [gl] gls.it.evar_hyps in
+  let hyps=make_hyps gamma gls [gl] 
+      (Environ.named_context_of_val gls.it.evar_hyps) in
   let formula=
     List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in  
   let search_fun = 
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index d98b3b6bd..6c3f87a5b 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -164,7 +164,7 @@ Ltac Make_ring_rw Cst_tac lemma req r :=
     let pe1 := mkPol r1 fv in
     let pe2 := mkPol r2 fv in
     ((apply (lemma1 fv pe1 pe2);
-      compute;
+      vm_compute;
       exact (refl_equal true)) ||
      (Make_ring_rewrite_step (lemma2 fv) pe1;
       Make_ring_rewrite_step (lemma2 fv) pe2))
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 573f83cea..6a78e88c7 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -195,10 +195,10 @@ let protect_red env sigma c =
     (mk_clos_but (is_ring_thm req) c);;
 
 let protect_tac =
-  Tactics.reduct_option protect_red None ;;
+  Tactics.reduct_option (protect_red,DEFAULTcast) None ;;
 
 let protect_tac_in id =
-  Tactics.reduct_option protect_red (Some(id,[],(InHyp, ref None)));;
+  Tactics.reduct_option (protect_red,DEFAULTcast) (Some(id,[],(InHyp, ref None)));;
 
 
 TACTIC EXTEND protect_fv
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 4f86af1e8..7b07abbc8 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -61,7 +61,7 @@ let etype_of_evar evs ev =
     | [] ->
 	let t' = subst_evars evs n ev.evar_concl in
 	  subst_vars acc 0 t'	
-  in aux [] 0 (rev ev.evar_hyps)
+  in aux [] 0 (rev (Environ.named_context_of_val ev.evar_hyps))
 
 
 open Tacticals
diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml
index dcca9361a..876dc68bb 100644
--- a/contrib/subtac/infer.ml
+++ b/contrib/subtac/infer.ml
@@ -552,7 +552,7 @@ let rec dtype_of_types ctx c =
       | Meta mv -> notimpl "Meta"
       | Evar pex -> notimpl "Evar"
       | Sort s -> DTSort (dummy_loc, s)
-      | Cast (c, t) -> snd (dtype_of_types ctx t)
+      | Cast (c, _, t) -> snd (dtype_of_types ctx t)
       | Prod (n, t, t') -> 
 	  let dt = dtype_of_types ctx t in
 	  let ctx' = (n, dt) :: ctx in
@@ -600,7 +600,7 @@ let rec dtype_of_constr ctx c =
       | Meta mv -> notimpl "Meta"
       | Evar pex -> notimpl "Evar"
       | Sort s -> DTSort (dummy_loc, s)
-      | Cast (c, t) -> snd (dtype_of_constr ctx t)
+      | Cast (_,_,t) -> snd (dtype_of_constr ctx t)
       | Prod (n, t, t') -> 
 	  let dt = dtype_of_constr ctx t in
 	  let ctx' = (n, dt) :: ctx in
diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
index c9a0a78c7..ce0f15ec2 100644
--- a/contrib/subtac/rewrite.ml
+++ b/contrib/subtac/rewrite.ml
@@ -349,7 +349,8 @@ and subset_coerce prog_info ctx x y =
 		let ctx', pcx' = subst_ctx ctx pcx in
 		  cx, {
 		    Evd.evar_concl = pcx';
-		    Evd.evar_hyps = evar_ctx prog_info ctx';
+		    Evd.evar_hyps = 
+                     Environ.val_of_named_context (evar_ctx prog_info ctx');
 		    Evd.evar_body = Evd.Evar_empty;
 		  }
 	      in
@@ -368,7 +369,7 @@ and subset_coerce prog_info ctx x y =
 		 in
 		   ignore(Univ.merge_constraints cstrs (Global.universes ()));
 		   Some (fun x ->
-			   mkCast (x, y))
+			   mkCast (x, DEFAULTcast, y))
 	       with 
 		   Reduction.NotConvertible ->	
 		     subtyping_error 
@@ -420,7 +421,9 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 			   let evarinfo = 
 			     { 
 			       Evd.evar_concl = proof;
-			       Evd.evar_hyps = evar_ctx prog_info ctx';
+			       Evd.evar_hyps = 
+			        Environ.val_of_named_context 
+				 (evar_ctx prog_info ctx');
 			       Evd.evar_body = Evd.Evar_empty;
 			     }
 			   in
@@ -581,7 +584,7 @@ let subtac recursive id (s, t) =
 		    let key = mknewexist () in
 		      prog_info.evm <- Evd.add prog_info.evm key 
 			{ Evd.evar_concl = wf_rel;
-			  Evd.evar_hyps = [];
+			  Evd.evar_hyps = Environ.empty_named_context_val;
 			  Evd.evar_body = Evd.Evar_empty };
 		      mkEvar (key, [| |])
 	    in
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 54510ba17..caac70310 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -263,7 +263,7 @@ let typeur sigma metamap =
     | T.App(f,args)->
         T.strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
-    | T.Cast (c,t) -> t
+    | T.Cast (c,_, t) -> t
     | T.Sort _ | T.Prod _ ->
        match sort_of env cstr with
           Coq_sort T.InProp -> T.mkProp
@@ -273,7 +273,7 @@ let typeur sigma metamap =
                                                                                 
   and sort_of env t =
     match Term.kind_of_term t with
-    | T.Cast (c,s) when T.isSort s -> family_of_term s
+    | T.Cast (c,_, s) when T.isSort s -> family_of_term s
     | T.Sort (T.Prop c) -> Coq_sort T.InType
     | T.Sort (T.Type u) -> Coq_sort T.InType
     | T.Prod (name,t,c2) ->
@@ -283,7 +283,7 @@ let typeur sigma metamap =
           | Coq_sort T.InSet, (Coq_sort T.InSet as s) -> s
           | Coq_sort T.InType, (Coq_sort T.InSet as s)
           | CProp, (Coq_sort T.InSet as s) when
-              Environ.engagement env = Some Environ.ImpredicativeSet -> s
+              Environ.engagement env = Some Declarations.ImpredicativeSet -> s
           | Coq_sort T.InType, Coq_sort T.InSet
           | CProp, Coq_sort T.InSet -> Coq_sort T.InType
           | _, (Coq_sort T.InType as s) -> s (*Type Univ.dummy_univ*)
@@ -295,7 +295,7 @@ let typeur sigma metamap =
                                                                                 
   and sort_family_of env t =
     match T.kind_of_term t with
-    | T.Cast (c,s) when T.isSort s -> family_of_term s
+    | T.Cast (c,_, s) when T.isSort s -> family_of_term s
     | T.Sort (T.Prop c) -> Coq_sort T.InType
     | T.Sort (T.Type u) -> Coq_sort T.InType
     | T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2
@@ -560,7 +560,7 @@ print_endline "PASSATO" ; flush stdout ;
                (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
            | T.Meta _ -> Util.anomaly "Meta met during exporting to XML"
            | T.Sort s -> A.ASort (fresh_id'', s)
-           | T.Cast (v,t) ->
+           | T.Cast (v,_, t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort then
                add_inner_type fresh_id'' ;
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index d4093f002..24676f186 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -42,7 +42,7 @@ prerr_endline "###whd_betadeltaiotacprop:" ;
 let xxx =
 (*Pp.msgerr (Printer.prterm_env env ty);*)
 prerr_endline "";
-   Redexpr.reduction_of_red_expr red_exp env evar_map ty
+   (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty
 in
 prerr_endline "###FINE" ;
 (*
@@ -92,7 +92,8 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         let ty = Unshare.unshare (Evd.existential_type sigma ev) in
         let jty = execute env sigma ty None in
         let jty = assumption_of_judgment env sigma jty in
-        let evar_context = (Evd.map sigma n).Evd.evar_hyps in
+        let evar_context = 
+	  E.named_context_of_val (Evd.map sigma n).Evd.evar_hyps in
          let rec iter actual_args evar_context =
           match actual_args,evar_context with
              [],[] -> ()
@@ -230,11 +231,11 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
          let j3 = execute env1 sigma c3 None in
           Typeops.judge_of_letin env name j1 j2 j3
   
-     | T.Cast (c,t) ->
+     | T.Cast (c,k,t) ->
         let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in
         let tj = execute env sigma t None in
 	let tj = type_judgment env sigma tj in
-        let j, _ = Typeops.judge_of_cast env cj tj in
+        let j, _ = Typeops.judge_of_cast env cj k tj in
 	 j
     in
      let synthesized = E.j_type judgement in
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 9220e8a4d..f78df7478 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -32,7 +32,7 @@ let nf_evar sigma ~preserve =
     match T.kind_of_term t with
      | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _
      | T.Construct _ -> t
-     | T.Cast (c1,c2) -> T.mkCast (aux c1, aux c2)
+     | T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2)
      | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2)
      | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c)
      | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c)
@@ -41,7 +41,7 @@ let nf_evar sigma ~preserve =
         let l' = Array.map aux l in
          (match T.kind_of_term c' with
              T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
-           | T.Cast (he,_) ->
+           | T.Cast (he,_,_) ->
               (match T.kind_of_term he with
                   T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
                 | _ -> T.mkApp (c', l')
@@ -123,18 +123,22 @@ let extract_open_proof sigma pf =
 (*CSC: it becomes a Rel; otherwise a Var. Then it can be already used  *)
 (*CSC: as the evar_instance. Ordering the instance becomes useless (it *)
 (*CSC: will already be ordered.                                        *)
-             (Termops.ids_of_named_context goal.Evd.evar_hyps) in
+             (Termops.ids_of_named_context 
+		(Environ.named_context_of_val goal.Evd.evar_hyps)) in
 	 let sorted_rels =
 	   Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in
 	 let context =
-          List.map
-            (fun (_,id) -> Sign.lookup_named id goal.Evd.evar_hyps)
-            sorted_rels
+	   let l = 
+             List.map
+               (fun (_,id) -> Sign.lookup_named id 
+		   (Environ.named_context_of_val goal.Evd.evar_hyps))
+               sorted_rels in
+	   Environ.val_of_named_context l
          in
 (*CSC: the section variables in the right order must be added too *)
          let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in
-         let env = Global.env_of_context context in
-         let evd',evar =
+    (*     let env = Global.env_of_context context in *)
+	 let evd',evar =
            Evarutil.new_evar_instance context !evd goal.Evd.evar_concl
              evar_instance in
          evd := evd' ;
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 423991784..b9d920903 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -46,7 +46,8 @@ let constr_to_xml obj sigma env =
   let rel_context = Sign.push_named_to_rel_context named_context' [] in
   let rel_env =
    Environ.push_rel_context rel_context
-    (Environ.reset_with_named_context real_named_context env) in
+    (Environ.reset_with_named_context 
+	(Environ.val_of_named_context real_named_context) env) in
   let obj' =
    Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in
   let seed = ref 0 in
@@ -180,11 +181,12 @@ Pp.ppnl (Pp.(++) (Pp.str
                     (constr_to_xml tid sigma env))
                >] in
          let old_names = List.map (fun (id,c,tid)->id) old_hyps in
+	 let nhyps = Environ.named_context_of_val hyps in
          let new_hyps =
-          List.filter (fun (id,c,tid)-> not (List.mem id old_names)) hyps in
+          List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in
 
          X.xml_nempty "Tactic" of_attribute
-          [<(build_hyps new_hyps) ; (aux flat_proof hyps)>]
+          [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
         end
 
      | {PT.ref=Some(PT.Change_evars,nodes)} ->
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index e8f149402..96f73abe0 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -290,7 +290,7 @@ let find_hyps t =
     | T.Meta _
     | T.Evar _
     | T.Sort _ -> l
-    | T.Cast (te,ty) -> aux (aux l te) ty
+    | T.Cast (te,_, ty) -> aux (aux l te) ty
     | T.Prod (_,s,t) -> aux (aux l s) t
     | T.Lambda (_,s,t) -> aux (aux l s) t
     | T.LetIn (_,s,_,t) -> aux (aux l s) t
@@ -359,7 +359,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env =
                (* t will not be exported to XML. Thus no unsharing performed *)
                final_var_ids,(n, Acic.Def  (Unshare.unshare b',t))::tl'
         in
-         aux [] (List.rev evar_hyps)
+         aux [] (List.rev (Environ.named_context_of_val evar_hyps))
        in
         (* We map the named context to a rel context and every Var to a Rel *)
         (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))