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

9 files changed, 43 insertions, 45 deletions

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
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index aa5e132c67..c1c3e3a186 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -263,9 +263,9 @@ let typecheck_inductive env mie =
 	  (* conclusions of the parameters *)
           (* We enforce [u >= lev] in case [lev] has a strict upper *)
           (* constraints over [u] *)
-	  Inr (param_ccls, lev), enforce_geq u lev cst
+	  Inr (param_ccls, lev), enforce_leq lev u cst
       | Type u (* Not an explicit occurrence of Type *) ->
-	  Inl (info,full_arity,s), enforce_geq u lev cst
+	  Inl (info,full_arity,s), enforce_leq lev u cst
       | Prop Pos when engagement env <> Some ImpredicativeSet ->
 	  (* Predicative set: check that the content is indeed predicative *)
 	  if not (is_type0m_univ lev) & not (is_type0_univ lev) then
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
 
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e2ef7aa15d..3c8ad0606e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -335,13 +335,25 @@ let is_lt g arcu arcv = (compare g arcu arcv = LT)
    Adding u>v is consistent iff compare(v,u) = NLE
     and then it is redundant iff compare(u,v) = LT *)
 
-(** * Universe checks [check_eq] and [check_geq], used in coqchk *)
+(** * Universe checks [check_eq] and [check_leq], used in coqchk *)
 
-let compare_eq g u v =
+(** First, checks on universe levels *)
+
+let check_equal g u v =
   let g, arcu = safe_repr g u in
   let _, arcv = safe_repr g v in
   arcu == arcv
 
+let check_smaller g strict u v =
+  let g, arcu = safe_repr g u in
+  let g, arcv = safe_repr g v in
+  if strict then
+    is_lt g arcu arcv
+  else
+    arcu == snd (safe_repr g UniverseLevel.Set) || is_leq g arcu arcv
+
+(** Then, checks on universes *)
+
 type check_function = universes -> universe -> universe -> bool
 
 let incl_list cmp l1 l2 =
@@ -350,36 +362,22 @@ let incl_list cmp l1 l2 =
 let compare_list cmp l1 l2 =
   incl_list cmp l1 l2 && incl_list cmp l2 l1
 
-let rec check_eq g u v =
-  match (u,v) with
-    | Atom ul, Atom vl -> compare_eq g ul vl
+let check_eq g u v =
+  match u,v with
+    | Atom ul, Atom vl -> check_equal g ul vl
     | Max(ule,ult), Max(vle,vlt) ->
         (* TODO: remove elements of lt in le! *)
-        compare_list (compare_eq g) ule vle &&
-        compare_list (compare_eq g) ult vlt
+        compare_list (check_equal g) ule vle &&
+        compare_list (check_equal g) ult vlt
     | _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *)
 
-let compare_greater g strict u v =
-  let g, arcu = safe_repr g u in
-  let g, arcv = safe_repr g v in
-  if strict then
-    is_lt g arcv arcu
-  else
-    arcv == snd (safe_repr g UniverseLevel.Set) || is_leq g arcv arcu
-
-(*
-let compare_greater g strict u v =
-  let b = compare_greater g strict u v in
-  ppnl(str (if b then if strict then ">" else ">=" else "NOT >="));
-  b
-*)
-let check_geq g u v =
-  match u, v with
-    | Atom ul, Atom vl -> compare_greater g false ul vl
-    | Atom ul, Max(le,lt) ->
-        List.for_all (fun vl -> compare_greater g false ul vl) le &&
-        List.for_all (fun vl -> compare_greater g true ul vl) lt
-    | _ -> anomaly "check_greater"
+let check_leq g u v =
+  match u,v with
+    | Atom ul, Atom vl -> check_smaller g false ul vl
+    | Max(le,lt), Atom vl ->
+        List.for_all (fun ul -> check_smaller g false ul vl) le &&
+        List.for_all (fun ul -> check_smaller g true ul vl) lt
+    | _ -> anomaly "check_leq"
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
@@ -524,12 +522,12 @@ let constraint_add_leq v u c =
   if v = UniverseLevel.Set || UniverseLevel.equal v u then c
   else Constraint.add (v,Le,u) c
 
-let enforce_geq u v c =
+let enforce_leq u v c =
   match u, v with
-  | Atom u, Atom v -> constraint_add_leq v u c
-  | Atom u, Max (gel,gtl) ->
-      let d = List.fold_right (fun v -> constraint_add_leq v u) gel c in
-      List.fold_right (fun v -> Constraint.add (v,Lt,u)) gtl d
+  | Atom u, Atom v -> constraint_add_leq u v c
+  | Max (gel,gtl), Atom v ->
+      let d = List.fold_right (fun u -> constraint_add_leq u v) gel c in
+      List.fold_right (fun u -> Constraint.add (u,Lt,v)) gtl d
   | _ -> anomaly "A universe bound can only be a variable"
 
 let enforce_eq u v c =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e4e66915d1..2d1a660565 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -42,7 +42,7 @@ val sup   : universe -> universe -> universe
 type universes
 
 type check_function = universes -> universe -> universe -> bool
-val check_geq : check_function
+val check_leq : check_function
 val check_eq : check_function
 
 (** The empty graph of universes *)
@@ -60,7 +60,7 @@ val is_empty_constraint : constraints -> bool
 
 type constraint_function = universe -> universe -> constraints -> constraints
 
-val enforce_geq : constraint_function
+val enforce_leq : constraint_function
 val enforce_eq : constraint_function
 
 (** {6 ... } *)
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 =