diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 36f3349c0..454134f21 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -306,6 +306,8 @@ type 'a puniverses = 'a * universe_instance val out_punivs : 'a puniverses -> 'a val in_punivs : 'a -> 'a puniverses +val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool + (** A vector of universe levels with universe constraints, representiong local universe variables and associated constraints *) |