diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 10eccd059b..c1692f8e71 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -194,7 +194,7 @@ let sort_cmp pb s0 s1 cuniv = assert (is_univ_variable u2); (match pb with | CONV -> enforce_eq u1 u2 cuniv - | CUMUL -> enforce_geq u2 u1 cuniv) + | CUMUL -> enforce_leq u1 u2 cuniv) | (_, _) -> raise NotConvertible |