diff options
| author | ppedrot | 2013-05-09 18:54:11 +0000 |
|---|---|---|
| committer | ppedrot | 2013-05-09 18:54:11 +0000 |
| commit | 8fd5b51c3dc21a6ef4c996edd3968c3082274276 (patch) | |
| tree | 2d91509e4aa74a9c663a384c7dc687bc20e280f1 /lib | |
| parent | 78a5b30be750c517d529f9f2b8a291699d5d92e6 (diff) | |
Getting rid of module Gmapl.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/gmapl.ml | 33 | ||||
| -rw-r--r-- | lib/gmapl.mli | 21 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 |
3 files changed, 0 insertions, 55 deletions
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 |