From 9084393008d9cd2a1f36391e06f6a73cbc529a16 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 25 Sep 1999 14:33:49 +0000
Subject: ensembles de contraintes d'univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index ebb1e1f67..8a200aab0 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Names
+open Univ
 open Term
 open Inductive
 open Environ
@@ -18,5 +19,5 @@ val sort_of_arity : 'a unsafe_env -> constr -> sorts
 val cci_inductive : 
   'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool -> 
     (identifier * typed_type * identifier list * bool * bool * constr) list ->
-      mutual_inductive_body
-
+      constraints ->
+      	mutual_inductive_body
-- 
cgit v1.2.3