equal
deleted
inserted
replaced
1 (* ========================================================================= *) |
1 (* ========================================================================= *) |
2 (* FINITE MAPS WITH A FIXED KEY TYPE *) |
2 (* FINITE MAPS WITH A FIXED KEY TYPE *) |
3 (* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *) |
3 (* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) |
4 (* ========================================================================= *) |
4 (* ========================================================================= *) |
5 |
5 |
6 functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t = |
6 functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t = |
7 struct |
7 struct |
8 |
8 |