From 8fd5b51c3dc21a6ef4c996edd3968c3082274276 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 9 May 2013 18:54:11 +0000
Subject: Getting rid of module Gmapl.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/gmapl.ml  | 33 ---------------------------------
 lib/gmapl.mli | 21 ---------------------
 lib/lib.mllib |  1 -
 3 files changed, 55 deletions(-)
 delete mode 100644 lib/gmapl.ml
 delete mode 100644 lib/gmapl.mli

(limited to 'lib')

diff --git a/lib/gmapl.ml b/lib/gmapl.ml
deleted file mode 100644
index 4be8f4baf6..0000000000
--- a/lib/gmapl.ml
+++ /dev/null
@@ -1,33 +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        *)
-(************************************************************************)
-
-open Util
-
-type ('a,'b) t = ('a,'b list) Gmap.t
-
-let empty = Gmap.empty
-let mem = Gmap.mem
-let iter = Gmap.iter
-let map = Gmap.map
-let fold = Gmap.fold
-
-let add x y m =
-  try
-    let l = Gmap.find x m in
-    Gmap.add x (y::List.except y l) m
-  with Not_found ->
-    Gmap.add x [y] m
-
-let find x m =
-  try Gmap.find x m with Not_found -> []
-
-let remove x y m =
-  let l = Gmap.find x m in
-  Gmap.add x (if List.mem y l then List.subtract l [y] else l) m
-
-
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
deleted file mode 100644
index 5e77208863..0000000000
--- a/lib/gmapl.mli
+++ /dev/null
@@ -1,21 +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 from ['a] to lists of ['b]. *)
-
-type ('a,'b) t
-
-val empty : ('a,'b) t
-val mem :  'a -> ('a,'b) t -> bool
-val iter : ('a -> 'b list -> unit) -> ('a,'b) t -> unit
-val map : ('b list -> 'c list) -> ('a,'b) t -> ('a,'c) t
-val fold : ('a -> 'b list -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
-
-val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
-val find : 'a -> ('a,'b) t -> 'b list
-val remove : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 0ff2d97e95..088bbf0102 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -12,7 +12,6 @@ Gmap
 Fset
 Fmap
 Tries
-Gmapl
 Profile
 Explore
 Predicate
-- 
cgit v1.2.3