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
---
 kernel/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b5d825e843..af237d1d12 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -630,7 +630,7 @@ let check_one_fix renv recpos def =
 
       (* The cases below simply check recursively the condition on the
          subterms *)
-      | Cast (a,b) -> 
+      | Cast (a,_, b) -> 
           List.for_all (check_rec_call renv) (a::b::l)
 
       | Lambda (x,a,b) ->
-- 
cgit v1.2.3