From f4c935fffa04b2007d8d8bf7b9eafc3a72ac8cf4 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 22 Mar 2012 13:22:09 +0000
Subject: 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
---
 checker/mod_checking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index cc9ca9031..b49db27c3 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -22,7 +22,7 @@ let refresh_arity ar =
       Sort (Type u) when not (Univ.is_univ_variable u) ->
         let u' = Univ.fresh_local_univ() in
         mkArity (ctxt,Type u'),
-        Univ.enforce_geq u' u Univ.empty_constraint
+        Univ.enforce_leq u u' Univ.empty_constraint
     | _ -> ar, Univ.empty_constraint
 
 let check_constant_declaration env kn cb =
-- 
cgit v1.2.3