From f2da732ffd5db2b93a2c8120c668f8b2f6068d3b Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 Dec 1999 14:56:36 +0000
Subject: debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas
 linkes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 433a2c1d95..5ab2886a97 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -121,7 +121,8 @@ let mind_check_names mie =
    declaration, and checks that they are all present (and all the same)
    for all the given types. *)
 
-let mind_extract_params = decompose_prod_n
+let mind_extract_params n c = 
+  let (l,c') = decompose_prod_n n c in (List.rev l,c')
   
 let extract nparams c =
   try mind_extract_params nparams c 
-- 
cgit v1.2.3