From 31b99c5671c956de455372e43f935e1c70006f9d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Jul 2014 15:49:03 +0200 Subject: Export type_of_global_ref (useful for external users of glob files) --- interp/dumpglob.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'interp/dumpglob.mli') 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 -- cgit v1.2.3