From 49c4c49a402c6ec826a506903fcfab1bbd96e080 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 26 Nov 2012 15:52:30 +0000
Subject: 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
---
 kernel/indtypes.ml |  3 +--
 kernel/term.ml     | 17 +++++++++++++++--
 kernel/term.mli    |  1 +
 3 files changed, 17 insertions(+), 4 deletions(-)

(limited to 'kernel')

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. } *)
-- 
cgit v1.2.3