From 2fa42e57ecc5e8170e36fb63919f4b0a9ad19430 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 21 Nov 2008 20:23:05 +0000
Subject: fixed problem with r11612

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 2ac913607a..46969ec831 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1145,7 +1145,21 @@ let array_fold_map2' f v1 v2 e =
   in
   (v',!e')
 
+(* N.logN *)
 let array_distinct v =
+  let visited = Hashtbl.create 23 in
+  try
+    Array.iter
+      (fun x ->
+        if Hashtbl.mem visited h then raise Exit
+        else Hashtbl.add visited h h)
+      v;
+    true
+  with Exit -> false
+
+
+(* quadratic *)
+(*let array_distinct v =
   try
     for i=0 to Array.length v-1 do
       for j=i+1 to Array.length v-1 do
@@ -1155,6 +1169,7 @@ let array_distinct v =
     true
   with Exit ->
     false
+*)
 
 let array_union_map f a acc =
   Array.fold_left
-- 
cgit v1.2.3