diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /lib/gmapl.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'lib/gmapl.ml')
-rw-r--r-- | lib/gmapl.ml | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/lib/gmapl.ml b/lib/gmapl.ml new file mode 100644 index 00000000..dcb2eb94 --- /dev/null +++ b/lib/gmapl.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: gmapl.ml,v 1.2.16.1 2004/07/16 19:30:29 herbelin Exp $ *) + +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 (if List.mem y l then l else 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 + + |