Manual coding of Int.Map.find. We use unsafe features, but this function

is quite critical indeed, as it is one of the most used throughout Coq
executions.

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

1 files changed, 19 insertions, 1 deletions

diff --git a/lib/int.ml b/lib/int.ml
index b5519a5715..952d04e9bd 100644
--- a/lib/int.ml
+++ b/lib/int.ml
@@ -21,7 +21,25 @@ struct
 end
 
 module Set = Set.Make(Self)
-module Map = CMap.Make(Self)
+module Map =
+struct
+  include CMap.Make(Self)
+
+  type 'a map = 'a CMap.Make(Self).t
+
+  type 'a _map =
+  | MEmpty
+  | MNode of 'a map * int * 'a * 'a map * int
+
+  let map_prj : 'a map -> 'a _map = Obj.magic
+
+  let rec find i s = match map_prj s with
+  | MEmpty -> raise Not_found
+  | MNode (l, k, v, r, h) ->
+    if i < k then find i l
+    else if i = k then v
+    else find i r
+end
 
 module List = struct
   let mem = List.memq