Fix extraction taking a type in the wrong environment.

Fix restriction of universe contexts to not forget about potentially useful
constraints.

1 files changed, 2 insertions, 0 deletions

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