From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 kernel/univ.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 775e505f..df06e9af 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
+(* $Id: univ.ml 9507 2007-01-20 08:09:54Z herbelin $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -134,6 +134,10 @@ let is_base_univ = function
   | Max ([Base],[]) -> warning "Non canonical Set"; true
   | u -> false
 
+let is_univ_variable = function
+  | Atom a when a<>Base -> true
+  | _ -> false
+
 (* When typing [Prop] and [Set], there is no constraint on the level,
    hence the definition of [prop_univ], the type of [Prop] *)
 
-- 
cgit v1.2.3