diff options
Diffstat (limited to 'utils/tbl.mli')
| -rw-r--r-- | utils/tbl.mli | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/utils/tbl.mli b/utils/tbl.mli deleted file mode 100644 index 9ab22e0cba..0000000000 --- a/utils/tbl.mli +++ /dev/null @@ -1,12 +0,0 @@ -(* Association tables from any ordered type to any type. - We use the generic ordering to compare keys. *) - -type ('a, 'b) t - -val empty: ('a, 'b) t -val add: 'a -> 'b -> ('a, 'b) t -> ('a, 'b) t -val find: 'a -> ('a, 'b) t -> 'b - -val iter: ('a -> 'b -> 'c) -> ('a, 'b) t -> unit - -val print: ('a -> unit) -> ('b -> unit) -> ('a, 'b) t -> unit |