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, 3 insertions, 3 deletions

diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 5e31d56755..e40cd2676e 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" ->