Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 61 insertions, 0 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
new file mode 100644
index 00000000..e15971eb
--- /dev/null
+++ b/kernel/univ.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+
+(* Universes. *)
+
+type universe
+
+val prop_univ : universe
+val make_univ : Names.dir_path * int -> universe
+
+(* The type of a universe *)
+val super : universe -> universe
+(* The max of 2 universes *)
+val sup   : universe -> universe -> universe
+
+(*s Graphs of universes. *)
+
+type universes
+
+(* The empty graph of universes *)
+val initial_universes : universes
+
+(*s Constraints. *)
+
+module Constraint : Set.S
+
+type constraints = Constraint.t
+
+type constraint_function = universe -> universe -> constraints -> constraints
+
+val enforce_geq : constraint_function
+val enforce_eq : constraint_function
+
+(*s Merge of constraints in a universes graph. 
+  The function [merge_constraints] merges a set of constraints in a given
+  universes graph. It raises the exception [UniverseInconsistency] if the
+  constraints are not satisfiable. *)
+
+exception UniverseInconsistency
+
+val merge_constraints : constraints -> universes -> universes
+
+(*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
+
+val hcons1_univ : universe -> universe