diff options
Diffstat (limited to 'typing/ident.mli')
| -rw-r--r-- | typing/ident.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/typing/ident.mli b/typing/ident.mli index 0e011ad0d..0405eff57 100644 --- a/typing/ident.mli +++ b/typing/ident.mli @@ -40,6 +40,9 @@ val hide: t -> t val make_global: t -> unit val global: t -> bool +val binding_time: t -> int +val current_time: unit -> int + val print: t -> unit type 'a tbl @@ -50,4 +53,5 @@ val add: t -> 'a -> 'a tbl -> 'a tbl val find_same: t -> 'a tbl -> 'a val find_name: string -> 'a tbl -> 'a +val iter: (t -> 'a -> unit) -> 'a tbl -> unit val print_tbl: ('a -> unit) -> 'a tbl -> unit |