From 90a2126b2fb2738a7684864e74e0d1ed3c861a98 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 15:41:30 +0200
Subject: Univs: the stdlib now needs 5 universes

Prop < Set < i for every global univ i
---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 39c36d5414..31b2129001 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -388,7 +388,7 @@ misc/deps-order.log:
 	} > "$@"
 
 # Sort universes for the whole standard library
-EXPECTED_UNIVERSES := 3
+EXPECTED_UNIVERSES := 5
 universes: misc/universes.log
 misc/universes.log: misc/universes/all_stdlib.v
 	@echo "TEST      misc/universes"
-- 
cgit v1.2.3