Gmap is now useless, hail to Map!

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

4 files changed, 0 insertions, 170 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index be0a2e5ec..e76162134 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -27,7 +27,6 @@ Dyn
 CUnix
 System
 Envars
-Gmap
 Profile
 Explore
 Predicate
diff --git a/lib/gmap.ml b/lib/gmap.ml
deleted file mode 100644
index 65971b237..000000000
--- a/lib/gmap.ml
+++ /dev/null
@@ -1,140 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Maps using the generic comparison function of ocaml. Code borrowed from
-   the ocaml standard library (Copyright 1996, INRIA). *)
-
-    type ('a,'b) t =
-        Empty
-      | Node of ('a,'b) t * 'a * 'b * ('a,'b) t * int
-
-    let empty = Empty
-
-    let is_empty = function Empty -> true | _ -> false
-
-    let height = function
-        Empty -> 0
-      | Node(_,_,_,_,h) -> h
-
-    let create l x d r =
-      let hl = height l and hr = height r in
-      Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
-
-    let bal l x d r =
-      let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
-      let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
-      if hl > hr + 2 then begin
-        match l with
-          Empty -> invalid_arg "Map.bal"
-        | Node(ll, lv, ld, lr, _) ->
-            if height ll >= height lr then
-              create ll lv ld (create lr x d r)
-            else begin
-              match lr with
-                Empty -> invalid_arg "Map.bal"
-              | Node(lrl, lrv, lrd, lrr, _)->
-                  create (create ll lv ld lrl) lrv lrd (create lrr x d r)
-            end
-      end else if hr > hl + 2 then begin
-        match r with
-          Empty -> invalid_arg "Map.bal"
-        | Node(rl, rv, rd, rr, _) ->
-            if height rr >= height rl then
-              create (create l x d rl) rv rd rr
-            else begin
-              match rl with
-                Empty -> invalid_arg "Map.bal"
-              | Node(rll, rlv, rld, rlr, _) ->
-                  create (create l x d rll) rlv rld (create rlr rv rd rr)
-            end
-      end else
-        Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
-
-    let rec add x data = function
-        Empty ->
-          Node(Empty, x, data, Empty, 1)
-      | Node(l, v, d, r, h) ->
-          let c = Pervasives.compare x v in
-          if Int.equal c 0 then
-            Node(l, x, data, r, h)
-          else if c < 0 then
-            bal (add x data l) v d r
-          else
-            bal l v d (add x data r)
-
-    let rec find x = function
-        Empty ->
-          raise Not_found
-      | Node(l, v, d, r, _) ->
-          let c = Pervasives.compare x v in
-          if Int.equal c 0 then d
-          else find x (if c < 0 then l else r)
-
-    let rec mem x = function
-        Empty ->
-          false
-      | Node(l, v, d, r, _) ->
-          let c = Pervasives.compare x v in
-          Int.equal c 0 || mem x (if c < 0 then l else r)
-
-    let rec min_binding = function
-        Empty -> raise Not_found
-      | Node(Empty, x, d, r, _) -> (x, d)
-      | Node(l, x, d, r, _) -> min_binding l
-
-    let rec remove_min_binding = function
-        Empty -> invalid_arg "Map.remove_min_elt"
-      | Node(Empty, x, d, r, _) -> r
-      | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
-
-    let merge t1 t2 =
-      match (t1, t2) with
-        (Empty, t) -> t
-      | (t, Empty) -> t
-      | (_, _) ->
-          let (x, d) = min_binding t2 in
-          bal t1 x d (remove_min_binding t2)
-
-    let rec remove x = function
-        Empty ->
-          Empty
-      | Node(l, v, d, r, h) ->
-          let c = Pervasives.compare x v in
-          if Int.equal c 0 then
-            merge l r
-          else if c < 0 then
-            bal (remove x l) v d r
-          else
-            bal l v d (remove x r)
-
-    let rec iter f = function
-        Empty -> ()
-      | Node(l, v, d, r, _) ->
-          iter f l; f v d; iter f r
-
-    let rec map f = function
-        Empty               -> Empty
-      | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h)
-
-    (* Maintien de fold_right par compatibilité (changé en fold_left dans
-       ocaml-3.09.0) *)
-
-    let rec fold f m accu =
-      match m with
-        Empty -> accu
-      | Node(l, v, d, r, _) ->
-          fold f l (f v d (fold f r accu))
-
-(* Added with respect to ocaml standard library. *)
-
-    let dom m = fold (fun x _ acc -> x::acc) m []
-
-    let rng m = fold (fun _ y acc -> y::acc) m []
-
-    let to_list m = fold (fun x y acc -> (x,y)::acc) m []
-
diff --git a/lib/gmap.mli b/lib/gmap.mli
deleted file mode 100644
index 06fbd6386..000000000
--- a/lib/gmap.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Maps using the generic comparison function of ocaml. Same interface as
-   the module [Map] from the ocaml standard library. *)
-
-type ('a,'b) t
-
-val empty : ('a,'b) t
-val is_empty : ('a,'b) t -> bool
-val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
-val find : 'a -> ('a,'b) t -> 'b
-val remove : 'a -> ('a,'b) t -> ('a,'b) t
-val mem :  'a -> ('a,'b) t -> bool
-val iter : ('a -> 'b -> unit) -> ('a,'b) t -> unit
-val map : ('b -> 'c) -> ('a,'b) t -> ('a,'c) t
-val fold : ('a -> 'b -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
-
-(** Additions with respect to ocaml standard library. *)
-
-val dom : ('a,'b) t -> 'a list
-val rng : ('a,'b) t -> 'b list
-val to_list : ('a,'b) t -> ('a * 'b) list
diff --git a/lib/lib.mllib b/lib/lib.mllib
index c5f828573..be27eed7d 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -8,7 +8,6 @@ Segmenttree
 Unicodetable
 Unicode
 System
-Gmap
 Trie
 Profile
 Explore