diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 96e3cabd42..46ee8d97e1 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -198,7 +198,7 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - if engagement env = Some StronglyConstructive then + if engagement env = Some ImpredicativeSet then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort else |