From 970b4b750486ad8544b5d0a3b2246282690e6c98 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Oct 2000 16:08:20 +0000
Subject: Correction incompatibilites dans la fn des types des inductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 4cfb3e2aba..0c8b15e3ce 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -55,8 +55,8 @@ type one_inductive_body = {
   mind_typename : identifier;
   mind_nf_lc : typed_type array; (* constrs and arity with pre-expanded ccl *)
   mind_nf_arity : typed_type;
-  mind_user_lc : constr array option;
-  mind_user_arity : constr option;
+  mind_user_lc : typed_type array option;
+  mind_user_arity : typed_type option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -73,8 +73,8 @@ type mutual_inductive_body = {
   mind_nparams : int }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
-val mind_user_lc : one_inductive_body -> constr array
-val mind_user_arity : one_inductive_body -> constr
+val mind_user_lc : one_inductive_body -> typed_type array
+val mind_user_arity : one_inductive_body -> typed_type
 val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body
 
 (*s Declaration of inductive types. *)
-- 
cgit v1.2.3