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

1 files changed, 5 insertions, 4 deletions

diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index d4093f002c..24676f1866 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