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

5 files changed, 29 insertions, 22 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 54510ba179..caac703108 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 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
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 9220e8a4db..f78df74789 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 4239917845..b9d9209038 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 e8f149402d..96f73abe0e 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))