diff options
| author | letouzey | 2012-03-22 13:22:09 +0000 |
|---|---|---|
| committer | letouzey | 2012-03-22 13:22:09 +0000 |
| commit | f4c935fffa04b2007d8d8bf7b9eafc3a72ac8cf4 (patch) | |
| tree | 78e67bff2ae35c7007a489767ba82b532812ea72 /kernel/reduction.ml | |
| parent | 8ab3816d1a4302b576e7d9d144c70524d5528376 (diff) | |
Univ: enforce_leq instead of enforce_geq for more uniformity
Same for check_leq instead of check_geq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |