STM: when batch compiling a vo, assert we behave conservatively

This meas that the list of future_constraints in safe_env is empty,
meaning that nothing was delayed.

1 files changed, 11 insertions, 2 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 241e9d565..bf758b96b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -525,13 +525,22 @@ let build_module_body params restype senv =
     (constraints, imports, etc) *)
 
 let propagate_senv newdef newenv newresolver senv oldsenv =
+  let now_cst, later_cst = List.partition Future.is_val senv.future_cst in
+  (* This asserts that after Paral-ITP, standard vo compilation is behaving
+   * exctly as before: the same universe constraints are added to modules *)
+  if !Flags.compilation_mode = Flags.BuildVo &&
+     !Flags.async_proofs_mode = Flags.APoff then assert(later_cst = []);
   { oldsenv with
     env = newenv;
     modresolver = newresolver;
     revstruct = newdef::oldsenv.revstruct;
     modlabels = Label.Set.add (fst newdef) oldsenv.modlabels;
-    univ = Univ.union_constraints senv.univ oldsenv.univ;
-    future_cst = senv.future_cst @ oldsenv.future_cst;
+    univ =
+      List.fold_left (fun acc cst ->
+        Univ.union_constraints acc (Future.force cst))
+      (Univ.union_constraints senv.univ oldsenv.univ)
+      now_cst;
+    future_cst = later_cst @ oldsenv.future_cst;
     (* engagement is propagated to the upper level *)
     engagement = senv.engagement;
     imports = senv.imports;