diff options
Diffstat (limited to 'library/library.mli')
| -rw-r--r-- | library/library.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/library/library.mli b/library/library.mli index 0a3b7d10d..13d83a5c0 100644 --- a/library/library.mli +++ b/library/library.mli @@ -78,3 +78,6 @@ val try_locate_qualified_library : qualid located -> DirPath.t * string (** {6 Statistics: display the memory use of a library. } *) val mem : DirPath.t -> Pp.std_ppcmds + +(** {6 Native compiler. } *) +val native_name_from_filename : string -> string |