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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 210c5aa697..f1c278bd2d 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -539,11 +539,11 @@ let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 = else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))) | Type u, Prop c -> if c = Pos then - add_constraints d (Univ.enforce_geq Univ.type0_univ u Univ.empty_constraint) + add_constraints d (Univ.enforce_leq u Univ.type0_univ Univ.empty_constraint) else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)) | _, Type u -> if is_univ_var_or_set u then - add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint) + add_constraints d (Univ.enforce_leq u1 u2 Univ.empty_constraint) else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)) let is_univ_level_var us u = |