From b3d97c2147418f44fc704807d3812b04921591af Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 1 Oct 2015 15:36:57 +0200
Subject: Univs: fix bug #4251, handling of template polymorphic constants.

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

(limited to 'kernel/univ.mli')

diff --git a/kernel/univ.mli b/kernel/univ.mli
index ad33d597e..4cc8a2528 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -91,6 +91,9 @@ sig
   val is_level : t -> bool
   (** Test if the universe is a level or an algebraic universe. *)
 
+  val is_levels : t -> bool
+  (** Test if the universe is a lub of levels or contains +n's. *)
+
   val level : t -> Level.t option
   (** Try to get a level out of a universe, returns [None] if it
       is an algebraic universe. *)
-- 
cgit v1.2.3