From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

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

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 3791c3e1..11a5452c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 11063 2008-06-06 16:03:45Z soubiran $ *)
+(* $Id: univ.ml 11301 2008-08-04 19:41:18Z herbelin $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -550,6 +550,11 @@ let subst_large_constraint u u' v =
 let subst_large_constraints =
   List.fold_right (fun (u,u') -> subst_large_constraint u u')
 
+let no_upper_constraints u cst =
+  match u with
+  | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
+  | Max _ -> anomaly "no_upper_constraints"
+
 (* Pretty-printing *)
 
 let num_universes g =
-- 
cgit v1.2.3