diff options
Diffstat (limited to 'interp/dumpglob.mli')
| -rw-r--r-- | interp/dumpglob.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 14e5a81308..be1e3f05d2 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -49,3 +49,4 @@ val type_of_global_ref : Names.GlobRef.t -> string (** Registration of constant information *) val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit +val constant_kind : Names.Constant.t -> Decls.logical_kind |