From 71aa415282a93a6e23af3b824f8531c58d2d66bd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 18 Jan 2020 14:46:05 +0100
Subject: Fix #11421 computation of Set+2

---
 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 51440147ad..0712774576 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -345,8 +345,8 @@ struct
           (Level.is_prop u && not (Level.is_sprop v))
         else false
 
-    let successor (u,n) =
-      if Level.is_small u then type1
+    let successor (u,n as e) =
+      if is_small e then type1
       else (u, n + 1)
 
     let addn k (u,n as x) =
-- 
cgit v1.2.3