diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index ae7400337..5682940a0 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -308,6 +308,9 @@ sig (** Keeps the order of the instances *) val union : t -> t -> t + (* the number of universes in the context *) + val size : t -> int + end type universe_context = UContext.t |