From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 23 Apr 2008 08:04:53 +0000 (+0000)
Subject: Do NOT dare using Pervasives.compare on data structures containing URIs!
X-Git-Tag: make_still_working~5295
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0805c61933df87f5cfae63b94456a1f0518b06d0;p=helm.git

Do NOT dare using Pervasives.compare on data structures containing URIs!
Use UriManager.compare to get a 2x speed-up in type-checking setoids.
---

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 7aac62cff..fe9f01d53 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -50,7 +50,15 @@ type universe = int * UriManager.uri option
     
 module UniverseType = struct
   type t = universe
-  let compare = Pervasives.compare
+  let compare (n1,u1) (n2,u2) =
+   let ndiff = n1 - n2 in
+    if ndiff <> 0 then ndiff
+    else
+     match u1,u2 with
+        None, None -> 0
+      | Some u1, Some u2 -> UriManager.compare u1 u2
+      | None, Some _ -> 1
+      | Some _, None -> -1
 end
   
 module SOF = Set.Make(UniverseType)