From bf578ad5e2f63b7a36aeaef5e0597101db1bd24a Mon Sep 17 00:00:00 2001
From: gregoire
Date: Fri, 2 Dec 2005 10:01:15 +0000
Subject: 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
---
 contrib/extraction/extraction.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/extraction')

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6bc6673397..41619c85ff 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] *) 
-- 
cgit v1.2.3