diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index f39f05d9..f3af0861 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: univ.mli 8673 2006-03-29 21:21:52Z herbelin $ i*) +(*i $Id: univ.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) (* Universes. *) @@ -14,9 +14,10 @@ type universe val base_univ : universe val prop_univ : universe +val neutral_univ : universe val make_univ : Names.dir_path * int -> universe -val is_base : universe -> bool +val is_base_univ : universe -> bool (* The type of a universe *) val super : universe -> universe @@ -24,9 +25,6 @@ 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 @@ -58,10 +56,15 @@ val merge_constraints : constraints -> universes -> universes val fresh_local_univ : unit -> universe -val solve_constraints_system : universe array -> universe array -> +val solve_constraints_system : universe option array -> universe array -> universe array -val is_empty_universe : universe -> bool +val is_empty_univ : universe -> bool + +val subst_large_constraint : universe -> universe -> universe -> universe + +val subst_large_constraints : + (universe * universe) list -> universe -> universe (*s Pretty-printing of universes. *) |