selective join/export of the safe_environment

This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.

6 files changed, 39 insertions, 34 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index e13fb4f08..cf0f715be 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -292,11 +292,6 @@ let hcons_mind mib =
 
 (** {6 Stm machinery } *)
 
-let join_constant_body otab cb =
-  match cb.const_body with
-  | OpaqueDef o -> Opaqueproof.join_opaque otab o
-  | _ -> ()
-
 let string_of_side_effect = function
   | SEsubproof (c,_,_) -> Names.string_of_con c
   | SEscheme (cl,_) ->
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 497856676..ad3e8be4f 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -75,8 +75,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit
-
 (** {6 Hash-consing} *)
 
 (** Here, strictly speaking, we don't perform true hash-consing
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 585b38a08..d91505f89 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -611,21 +611,31 @@ let clean_bounded_mod_expr sign =
   if is_functor sign then collect_mbid MBIset.empty sign else sign
 
 (** {6 Stm machinery } *)
-
-let rec join_module otab mb =
-  implem_iter (join_signature otab) (join_expression otab) mb.mod_expr;
-  Option.iter (join_expression otab) mb.mod_type_alg;
-  join_signature otab mb.mod_type
-and join_modtype otab mt =
-  Option.iter (join_expression otab) mt.typ_expr_alg;
-  join_signature otab mt.typ_expr
-and join_field otab (l,body) = match body with
-  |SFBconst sb -> join_constant_body otab sb
-  |SFBmind _ -> ()
-  |SFBmodule m -> join_module otab m
-  |SFBmodtype m -> join_modtype otab m
-and join_structure otab struc = List.iter (join_field otab) struc
-and join_signature otab sign =
-  functor_iter (join_modtype otab) (join_structure otab) sign
-and join_expression otab me = functor_iter (join_modtype otab) (fun _ -> ()) me
+let join_constant_body except otab cb =
+  match cb.const_body with
+  | OpaqueDef o ->
+      (match Opaqueproof.uuid_opaque otab o with
+      | Some uuid when not(Future.UUIDSet.mem uuid except) ->
+          Opaqueproof.join_opaque otab o
+      | _ -> ())
+  | _ -> ()
+
+let join_structure except otab s =
+  let rec join_module mb =
+    implem_iter join_signature join_expression mb.mod_expr;
+    Option.iter join_expression mb.mod_type_alg;
+    join_signature mb.mod_type
+  and join_modtype mt =
+    Option.iter join_expression mt.typ_expr_alg;
+    join_signature mt.typ_expr
+  and join_field (l,body) = match body with
+    |SFBconst sb -> join_constant_body except otab sb
+    |SFBmind _ -> ()
+    |SFBmodule m -> join_module m
+    |SFBmodtype m -> join_modtype m
+  and join_structure struc = List.iter join_field struc
+  and join_signature sign =
+    functor_iter join_modtype join_structure sign
+  and join_expression me = functor_iter join_modtype (fun _ -> ()) me in
+  join_structure s
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 0009b859c..c3f3f2d58 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -80,7 +80,8 @@ val clean_bounded_mod_expr : module_signature -> module_signature
 
 (** {6 Stm machinery } *)
 
-val join_structure : Opaqueproof.opaquetab -> structure_body -> unit
+val join_structure :
+  Future.UUIDSet.t -> Opaqueproof.opaquetab -> structure_body -> unit
 
 (** {6 Errors } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 11079d25b..bef72340c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -238,10 +238,12 @@ let push_context ctx = add_constraints (Now (Univ.UContext.constraints ctx))
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
 
-let join_safe_environment e =
-  Modops.join_structure (Environ.opaque_tables e.env) e.revstruct;
+let join_safe_environment ?(except=Future.UUIDSet.empty) e =
+  Modops.join_structure except (Environ.opaque_tables e.env) e.revstruct;
   List.fold_left
-    (fun e fc -> add_constraints (Now (Future.join fc)) e)
+    (fun e fc ->
+       if Future.UUIDSet.mem (Future.uuid fc) except then e
+       else add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
 (** {6 Various checks } *)
@@ -745,11 +747,9 @@ let start_library dir senv =
     modvariant = LIBRARY;
     imports = senv.imports }
 
-let export compilation_mode senv dir =
+let export ?except senv dir =
   let senv =
-    try
-      if compilation_mode = Flags.BuildVi then { senv with future_cst = [] }
-      else join_safe_environment senv
+    try join_safe_environment ?except senv
     with e ->
       let e = Errors.push e in
       Errors.errorlabstrm "export" (Errors.print e)
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