diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-05-02 11:33:34 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:01 +0200 |
commit | ce11f55e27c8e4f98384aacd61ee67c593340195 (patch) | |
tree | 9537fb3faf09eb0bb67eef5a25be7cca2516040a /kernel/sorts.ml | |
parent | af533645b1033dc386d8ac99cc8c4b6491b0ca91 (diff) |
Fix extraction taking a type in the wrong environment.
Fix restriction of universe contexts to not forget about potentially useful
constraints.
Diffstat (limited to 'kernel/sorts.ml')
-rw-r--r-- | kernel/sorts.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 3ebd06dd8..bfcdc0b4d 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 |