From e3a0a4d58b74d2113485ceabe4235567fda962c8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Oct 2014 17:12:30 +0200 Subject: selective join/export of the safe_environment This generalizes the BuildVi flag and lets one choose which opaque proofs are done and which not. --- kernel/safe_typing.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 6edea363b..943cf3df8 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -48,7 +48,8 @@ val is_curmod_library : safe_environment -> bool (* safe_environment has functional data affected by lazy computations, * thus this function returns a new safe_environment *) -val join_safe_environment : safe_environment -> safe_environment +val join_safe_environment : + ?except:Future.UUIDSet.t -> safe_environment -> safe_environment (** {6 Enriching a safe environment } *) @@ -138,7 +139,7 @@ type native_library = Nativecode.global list val start_library : DirPath.t -> module_path safe_transformer val export : - Flags.compilation_mode -> + ?except:Future.UUIDSet.t -> safe_environment -> DirPath.t -> module_path * compiled_library * native_library -- cgit v1.2.3