diff options
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 89bcccef3..5ff471e69 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -72,7 +72,8 @@ type library_objects val register_library : library_name -> - Safe_typing.compiled_library -> library_objects -> Digest.t -> unit + Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> + Univ.constraints -> unit val get_library_symbols_tbl : library_name -> Nativecode.symbol array |