From efce61af32ff1b09a21dcf88bca7d6609a0bfd27 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 5 Oct 2015 17:22:31 +0200
Subject: Univs: fix bug #4288, Print Sorted generated backward < constraints.

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

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 73d323426b..34eb283d73 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1582,8 +1582,8 @@ let sort_universes orig =
   let sorted = LMap.fold fold compact UMap.empty in
   (** Add all [Type.n] nodes *)
   let fold i accu u =
-    if 0 < i then
-      let pred = types.(i - 1) in
+    if i < max then
+      let pred = types.(i + 1) in
       let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
       UMap.add u (Canonical arc) accu
     else accu
-- 
cgit v1.2.3