From 5e6145c871eea1e94566b252b4bfc4cd752f42d5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Oct 2013 22:17:07 +0000
Subject: cList: set-as-list functions are now with an explicit comparison

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/sorts.ml  |  2 ++
 kernel/sorts.mli |  2 ++
 kernel/univ.ml   | 14 +++++++-------
 3 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 88c99683e5..d2469c4fdd 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -44,6 +44,8 @@ let family = function
   | Prop Pos -> InSet
   | Type _ -> InType
 
+let family_equal = (==)
+
 module Hsorts =
   Hashcons.Make(
     struct
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index f15b7cba41..51e8a6f6c5 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -27,3 +27,5 @@ val is_prop : t -> bool
 val family : t -> family
 
 val hcons : t -> t
+
+val family_equal : family -> family -> bool
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ddb5dcbc63..aa6c9c4c8f 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -154,12 +154,12 @@ let sup u v =
 	if UniverseLevel.equal u v then Atom u else Max ([u;v],[])
     | u, Max ([],[]) -> u
     | Max ([],[]), v -> v
-    | Atom u, Max (gel,gtl) -> Max (List.add_set u gel,gtl)
-    | Max (gel,gtl), Atom v -> Max (List.add_set v gel,gtl)
+    | Atom u, Max (gel,gtl) -> Max (List.add_set UniverseLevel.equal u gel,gtl)
+    | Max (gel,gtl), Atom v -> Max (List.add_set UniverseLevel.equal v gel,gtl)
     | Max (gel,gtl), Max (gel',gtl') ->
-	let gel'' = List.union gel gel' in
-	let gtl'' = List.union gtl gtl' in
-	Max (List.subtract gel'' gtl'',gtl'')
+	let gel'' = List.union UniverseLevel.equal gel gel' in
+	let gtl'' = List.union UniverseLevel.equal gtl gtl' in
+	Max (List.subtract UniverseLevel.equal gel'' gtl'',gtl'')
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
@@ -865,11 +865,11 @@ let make_max = function
 
 let remove_large_constraint u = function
   | Atom u' as x -> if UniverseLevel.equal u u' then Max ([],[]) else x
-  | Max (le,lt) -> make_max (List.remove u le,lt)
+  | Max (le,lt) -> make_max (List.remove UniverseLevel.equal u le,lt)
 
 let is_direct_constraint u = function
   | Atom u' -> UniverseLevel.equal u u'
-  | Max (le,lt) -> List.mem u le
+  | Max (le,lt) -> List.mem_f UniverseLevel.equal u le
 
 (*
    Solve a system of universe constraint of the form
-- 
cgit v1.2.3