From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 kernel/univ.mli | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

(limited to 'kernel/univ.mli')

diff --git a/kernel/univ.mli b/kernel/univ.mli
index e15971eb..f39f05d9 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -6,20 +6,27 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: univ.mli,v 1.21.14.1 2004/07/16 19:30:28 herbelin Exp $ i*)
+(*i $Id: univ.mli 8673 2006-03-29 21:21:52Z herbelin $ i*)
 
 (* Universes. *)
 
 type universe
 
+val base_univ : universe
 val prop_univ : universe
 val make_univ : Names.dir_path * int -> universe
 
+val is_base : universe -> bool
+
 (* The type of a universe *)
 val super : universe -> universe
+
 (* The max of 2 universes *)
 val sup   : universe -> universe -> universe
 
+(* The max of an array of universes *)
+val sup_array : universe array -> universe
+
 (*s Graphs of universes. *)
 
 type universes
@@ -47,13 +54,20 @@ exception UniverseInconsistency
 
 val merge_constraints : constraints -> universes -> universes
 
+(*s Support for sort-polymorphic inductive types *)
+
+val fresh_local_univ : unit -> universe
+
+val solve_constraints_system : universe array -> universe array -> 
+  universe array
+
+val is_empty_universe : universe -> bool
+
 (*s Pretty-printing of universes. *)
 
 val pr_uni : universe -> Pp.std_ppcmds
 val pr_universes : universes -> Pp.std_ppcmds
 
-val string_of_univ : universe -> string
-
 (*s Dumping to a file *)
 
 val dump_universes : out_channel -> universes -> unit
-- 
cgit v1.2.3