From c4486dfda07b872d20746778df5c443b052b92b9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 9 Jul 2015 21:08:44 +0200 Subject: Native compiler: refactor code handling pre-computed values. Fixes #4139 (Not_found exception with Require in modules). --- kernel/safe_typing.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a57fb108c..1e9cdbda0 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -137,6 +137,8 @@ type compiled_library type native_library = Nativecode.global list +val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols + val start_library : DirPath.t -> module_path safe_transformer val export : @@ -146,7 +148,7 @@ val export : (* Constraints are non empty iff the file is a vi2vo *) val import : compiled_library -> Univ.universe_context_set -> vodigest -> - (module_path * Nativecode.symbol array) safe_transformer + module_path safe_transformer (** {6 Safe typing judgments } *) -- cgit v1.2.3