diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/gmapl.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/gmapl.mli b/lib/gmapl.mli index 27b465f83d..c3a55e8c1c 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -3,7 +3,7 @@ (* Maps from ['a] to lists of ['b]. *) -type ('a,'b) t = ('a,'b list) Gmap.t +type ('a,'b) t val empty : ('a,'b) t val mem : 'a -> ('a,'b) t -> bool |