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

2 files changed, 7 insertions, 6 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 6bae2537ed..5f3cda588a 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -214,7 +214,7 @@ let pr_binder_among_many pr_c = function
       pr_binder true pr_c (nal,t)
   | LocalRawDef (na,c) ->
       let c,topt = match c with
-        | CCast(_,c,t) -> c, t
+        | CCast(_,c,_,t) -> c, t
         | _ -> c, CHole dummy_loc in
       hov 1 (surround
         (pr_lname na ++ pr_opt_type pr_c topt ++
@@ -595,7 +595,7 @@ let rec pr sep inherited a =
   | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
-  | CCast (_,a,b) ->
+  | CCast (_,a,_,b) ->
       hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b),
       lcast
   | CNotation (_,"( _ )",[t]) ->
@@ -634,7 +634,7 @@ let rec prod_constr_expr c = function
 
 let rec strip_context n iscast t =
   if n = 0 then
-    [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
+    [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t
   else match t with
     | CLambdaN (loc,(nal,t)::bll,c) ->
 	let n' = List.length nal in
@@ -657,7 +657,7 @@ let rec strip_context n iscast t =
     | CArrow (loc,t,c) ->
 	let bl', c = strip_context (n-1) iscast c in
 	LocalRawAssum ([loc,Anonymous],t) :: bl', c 
-    | CCast (_,c,_) -> strip_context n false c
+    | CCast (_,c,_,_) -> strip_context n false c
     | CLetIn (_,na,b,c) -> 
 	let bl', c = strip_context (n-1) iscast c in
 	LocalRawDef (na,b) :: bl', c
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index a8d0b13903..1e4b261036 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -609,7 +609,7 @@ let rec pr_vernac = function
                   (bl2,body,mt())
               | Some ty ->
                   let bl2,body,ty' = extract_def_binders c ty in
-                  (bl2,CCast (dummy_loc,body,ty'),
+                  (bl2,CCast (dummy_loc,body,Term.DEFAULTcast,ty'),
                    spc() ++ str":" ++
                    pr_sep_com spc
                      (pr_type_env_n (Global.env()) (bl@bl2)) ty') in
@@ -791,7 +791,8 @@ let rec pr_vernac = function
                 spc() ++ str "{struct " ++ pr_name name ++ str"}"
               else mt() in
 	    let bl,ppc =
-              pr_lconstr_env_n rec_sign true bl (CCast(dummy_loc,def,type_)) in
+              pr_lconstr_env_n rec_sign true bl 
+		(CCast(dummy_loc,def,Term.DEFAULTcast,type_)) in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_type c) type_
             ++ str" :=" ++ brk(1,1) ++ ppc ++