From 85bd945e22abc31fec8f89da1779d94027323e91 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 10 Dec 1999 08:57:01 +0000
Subject: debug discharge et inductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@227 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 6ae5bb931d..e46be516a6 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -133,7 +133,7 @@ let check_params nparams params c =
   try
     List.iter2 
       (fun (n1,t1) (n2,t2) ->
-	 if n1 <> n2 || strip_outer_cast t1 <> strip_outer_cast t2 then
+	 if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
 	   raise (InductiveError BadEntry))
       eparams params
   with Invalid_argument _ ->
-- 
cgit v1.2.3