Removed some FIXME related to equality on universes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16007 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 23 insertions, 10 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ada7c2c512..1aa6e8cda1 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -245,8 +245,7 @@ let typecheck_inductive env mie =
     begin match kind_of_term c with
     | Sort (Type u) ->
       if List.mem (Some u) l then
-        (** FIXME *)
-        None :: List.map (function Some v when Pervasives.(=) u v -> None | x -> x) l
+        None :: List.map (function Some v when Universe.equal u v -> None | x -> x) l
       else
         Some u :: l
     | _ ->
diff --git a/kernel/term.ml b/kernel/term.ml
index 627919f09f..4eac04f2d3 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -63,6 +63,19 @@ let prop_sort = Prop Null
 let set_sort = Prop Pos
 let type1_sort = Type type1_univ
 
+let sorts_ord s1 s2 =
+  if s1 == s2 then 0 else
+  match s1, s2 with
+  | Prop c1, Prop c2 ->
+    begin match c1, c2 with
+    | Pos, Pos | Null, Null -> 0
+    | Pos, Null -> -1
+    | Null, Pos -> 1
+    end
+  | Type u1, Type u2 -> Universe.compare u1 u2
+  | Prop _, Type _ -> -1
+  | Type _, Prop _ -> 1
+
 let is_prop_sort = function
 | Prop Null -> true
 | _ -> false
@@ -566,7 +579,7 @@ let compare_constr f t1 t2 =
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0
-  | Sort s1, Sort s2 -> Int.equal (Pervasives.compare s1 s2) 0 (** FIXME **)
+  | Sort s1, Sort s2 -> Int.equal (sorts_ord s1 s2) 0
   | Cast (c1,_,_), _ -> f c1 t2
   | _, Cast (c2,_,_) -> f t1 c2
   | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
@@ -612,7 +625,7 @@ let constr_ord_int f t1 t2 =
     | Rel n1, Rel n2 -> Int.compare n1 n2
     | Meta m1, Meta m2 -> Int.compare m1 m2
     | Var id1, Var id2 -> id_ord id1 id2
-    | Sort s1, Sort s2 -> Pervasives.compare s1 s2
+    | Sort s1, Sort s2 -> sorts_ord s1 s2
     | Cast (c1,_,_), _ -> f c1 t2
     | _, Cast (c2,_,_) -> f t1 c2
     | Prod (_,t1,c1), Prod (_,t2,c2)
diff --git a/kernel/term.mli b/kernel/term.mli
index 85192e1f14..cb48fbbe32 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -21,6 +21,7 @@ val set_sort  : sorts
 val prop_sort : sorts
 val type1_sort  : sorts
 
+val sorts_ord : sorts -> sorts -> int
 val is_prop_sort : sorts -> bool
 
 (** {6 The sorts family of CCI. } *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ff4d2837b4..888e4e388b 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -171,7 +171,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	  (match s, s' with
 	   Prop x, Prop y when x == y -> None
 	   | Prop _, Type _ -> None
-	   | Type x, Type y when Pervasives.(=) x y -> None (* false *) (** FIXME **)
+	   | Type x, Type y when Univ.Universe.equal x y -> None (* false *)
 	   | _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
 	  let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1c9573ca31..8849f17699 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -514,15 +514,15 @@ let univ_of_sort = function
   | Prop Null -> Univ.type0m_univ
 
 let is_eq_sort s1 s2 =
-  if Pervasives.(=) s1 s2 then None (* FIXME *)
+  if Int.equal (sorts_ord s1 s2) 0 then None (* FIXME *)
   else
     let u1 = univ_of_sort s1
     and u2 = univ_of_sort s2 in
-      if Pervasives.(=) u1 u2 then None (* FIXME *)
+      if Univ.Universe.equal u1 u2 then None
       else Some (u1, u2)
 
 let is_univ_var_or_set u =
-  Univ.is_univ_variable u || Pervasives.(=) u Univ.type0_univ (** FIXME *)
+  Univ.is_univ_variable u || Univ.is_type0_univ u
 
 let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
   match is_eq_sort s1 s2 with
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index c9a6d0b5b6..973f85818c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -161,7 +161,7 @@ let new_Type_sort () = Type (new_univ ())
 let refresh_universes_gen strict t =
   let modified = ref false in
   let rec refresh t = match kind_of_term t with
-    | Sort (Type u) when strict || Pervasives.(<>) u Univ.type0m_univ -> (** FIXME *)
+    | Sort (Type u) when strict || not (Univ.is_type0m_univ u) ->
 	modified := true; new_Type ()
     | Prod (na,u,v) -> mkProd (na,u,refresh v)
     | _ -> t in
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 9a9c99c12c..cc455dfeb5 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -77,7 +77,7 @@ let rec process_vernac_interp_error = function
 	str " because" ++ spc() ++ Univ.pr_uni v ++
 	  prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ Univ.pr_uni v)
 	  p ++
-	  (if Pervasives.(=) (snd (List.last p)) u then mt() else (* FIXME *)
+	  (if Univ.Universe.equal (snd (List.last p)) u then mt() else
 	      (spc() ++ str "= " ++ Univ.pr_uni u)) in
     let msg =
       if !Constrextern.print_universes then