From f4c935fffa04b2007d8d8bf7b9eafc3a72ac8cf4 Mon Sep 17 00:00:00 2001
From: letouzey
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/indtypes.ml     | 4 ++--
 checker/mod_checking.ml | 2 +-
 checker/reduction.ml    | 2 +-
 checker/typeops.ml      | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'checker')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index e48fdb6ef0..c12c54cfd9 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -177,9 +177,9 @@ let check_predicativity env s small level =
       Type u, _ ->
         let u' = fresh_local_univ () in
         let cst =
-          merge_constraints (enforce_geq u' u empty_constraint)
+          merge_constraints (enforce_leq u u' empty_constraint)
             (universes env) in
-        if not (check_geq cst u' level) then
+        if not (check_leq cst level u') then
           failwith "impredicative Type inductive type"
     | Prop Pos, Some ImpredicativeSet -> ()
     | Prop Pos, _ ->
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index cc9ca90310..b49db27c37 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 =
diff --git a/checker/reduction.ml b/checker/reduction.ml
index c1eadcd64a..c7c3846fa1 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -154,7 +154,7 @@ let sort_cmp univ pb s0 s1 =
         if not
 	  (match pb with
             | CONV -> check_eq univ u1 u2
-	    | CUMUL -> check_geq univ u2 u1)
+	    | CUMUL -> check_leq univ u1 u2)
         then raise NotConvertible
     | (_, _) -> raise NotConvertible
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index b904e0b688..98f071fa04 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -256,7 +256,7 @@ let refresh_arity env ar =
   match hd with
       Sort (Type u) when not (is_univ_variable u) ->
         let u' = fresh_local_univ() in
-        let env' = add_constraints (enforce_geq u' u empty_constraint) env in
+        let env' = add_constraints (enforce_leq u u' empty_constraint) env in
         env', mkArity (ctxt,Type u')
     | _ -> env, ar
 
-- 
cgit v1.2.3