From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

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

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index e76b7b02..775e505f 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: univ.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -63,8 +63,8 @@ let pr_uni_level u = str (string_of_univ_level u)
 let pr_uni = function
   | Atom u -> 
       pr_uni_level u
-  | Max ([],[Base]) ->
-      int 1
+  | Max ([],[u]) ->
+      str "(" ++ pr_uni_level u ++ str ")+1"
   | Max (gel,gtl) ->
       str "max(" ++ hov 0
        (prlist_with_sep pr_coma pr_uni_level gel ++
-- 
cgit v1.2.3