diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-10 15:49:03 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-11 10:15:06 +0200 |
| commit | 31b99c5671c956de455372e43f935e1c70006f9d (patch) | |
| tree | 2cdb46f8641b0ce89c8bb32284f7d459f13044dc /interp/dumpglob.mli | |
| parent | 024c980ab64e0d1102a10fdd793339c1dc84ac0f (diff) | |
Export type_of_global_ref (useful for external users of glob files)
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 28ada9fd9..efc861c36 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -41,3 +41,4 @@ val dump_constraint : val dump_string : string -> unit +val type_of_global_ref : Globnames.global_reference -> string |