From ce11f55e27c8e4f98384aacd61ee67c593340195 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 2 May 2014 11:33:34 +0200
Subject: Fix extraction taking a type in the wrong environment. Fix
 restriction of universe contexts to not forget about potentially useful
 constraints.

---
 kernel/sorts.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel')

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 3ebd06dd87..bfcdc0b4df 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -47,10 +47,12 @@ let equal s1 s2 = Int.equal (compare s1 s2) 0
 
 let is_prop = function
   | Prop Null -> true
+  | Type u when Universe.equal Universe.type0m u -> true
   | _ -> false
 
 let is_set = function
   | Prop Pos -> true
+  | Type u when Universe.equal Universe.type0 u -> true
   | _ -> false
 
 let is_small = function
-- 
cgit v1.2.3