diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d6bc6eb717..55b82e2148 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -615,10 +615,10 @@ let sort_cmp = sort_cmp let base_sort_cmp pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> c1 = c2 + | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos (* Prop <= Set *) | (Prop c1, Type u) -> pb = CUMUL | (Type u1, Type u2) -> true - | (Type u, Prop _) -> u = lower_univ & pb = CUMUL + | _ -> false let test_conversion f env sigma x y = |