vi2vo: universes handling finally fixed

Universes that are computed in the vi2vo step are not part of the
outermost module stocked in the vo file.  They are part of the
Library.seg_univ segment and are hence added to the safe env when
the vo file is loaded.

The seg_univ has been augmented.  It is now:
- an array of universe constraints, one for each constant whose opaque
  body was computed in the vi2vo phase.  This is useful only to print
  the constants (and its associated constraints).
- a union of all the constraints that come from proofs generated in the
  vi2vo phase.  This is morally the missing bits in the toplevel module
  body stocked in the vo file, and is there to ease the loading of
  a .vo file (obtained from a .vi file).
- a boolean, false if the file is incomplete (.vi) and true if it is
  complete (.vo obtained via vi2vo).

19 files changed, 128 insertions, 75 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 85324ec44..668ee3705 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -45,7 +45,8 @@ type library_t = {
   library_compiled : Cic.compiled_library;
   library_opaques : Cic.opaque_table;
   library_deps : Cic.library_deps;
-  library_digest : Digest.t }
+  library_digest : Cic.vodigest;
+  library_extra_univs : Univ.constraints }
 
 module LibraryOrdered =
   struct
@@ -112,11 +113,11 @@ let check_one_lib admit (dir,m) =
   if LibrarySet.mem dir admit then
     (Flags.if_verbose ppnl
       (str "Admitting library: " ++ pr_dirpath dir);
-      Safe_typing.unsafe_import file md dig)
+      Safe_typing.unsafe_import file md m.library_extra_univs dig)
   else
     (Flags.if_verbose ppnl
       (str "Checking library: " ++ pr_dirpath dir);
-      Safe_typing.import file md dig);
+      Safe_typing.import file md m.library_extra_univs dig);
   Flags.if_verbose pp (fnl());
   pp_flush ();
   register_loaded_library m
@@ -290,13 +291,14 @@ let with_magic_number_check f a =
 
 open Cic
 
-let mk_library md f table digest = {
+let mk_library md f table digest cst = {
   library_name = md.md_name;
   library_filename = f;
   library_compiled = md.md_compiled;
   library_opaques = table;
   library_deps = md.md_deps;
-  library_digest = digest }
+  library_digest = digest;
+  library_extra_univs = cst }
 
 let name_clash_message dir mdir f =
   str ("The file " ^ f ^ " contains library") ++ spc () ++
@@ -312,7 +314,7 @@ let intern_from_file (dir, f) =
     try
       let ch = with_magic_number_check raw_intern_library f in
       let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
-      let (opaque_csts:'a option), _, _ = System.marshal_in_segment f ch in
+      let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
       let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
       let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
       let (table:Cic.opaque_table), pos, checksum =
@@ -331,21 +333,30 @@ let intern_from_file (dir, f) =
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
         pp (str " (was a vi file) ");
-        Validate.validate !Flags.debug Values.v_univopaques opaque_csts
+      Option.iter (fun (_,_,b) -> if not b then
+        errorlabstrm "intern_from_file"
+          (str "The file "++str f++str " is still a .vi"))
+        opaque_csts;
+      Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
       end;
       (* Verification of the unmarshalled values *)
       Validate.validate !Flags.debug Values.v_lib md;
       Validate.validate !Flags.debug Values.v_opaques table;
       Flags.if_verbose ppnl (str" done]"); pp_flush ();
+      let digest =
+        if opaque_csts <> None then Cic.Dvivo (digest,udg)
+        else (Cic.Dvo digest) in
       md,table,opaque_csts,digest
     with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
   opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
-  Option.iter (fun opaque_csts ->
+  Option.iter (fun (opaque_csts,_,_) ->
     opaque_univ_tables :=
       LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
     opaque_csts;
-  mk_library md f table digest
+  let extra_cst =
+    Option.default Univ.empty_constraint (Option.map pi2 opaque_csts) in
+  mk_library md f table digest extra_cst
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
diff --git a/checker/cic.mli b/checker/cic.mli
index 8e6c5580d..bfea85327 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -362,7 +362,11 @@ type nativecode_symb_array
 
 type compilation_unit_name = DirPath.t
 
-type library_info = compilation_unit_name * Digest.t
+type vodigest =
+  | Dvo of Digest.t              (* The digest of the seg_lib part *)
+  | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+type library_info = compilation_unit_name * vodigest
 
 type library_deps = library_info array
 
@@ -388,7 +392,8 @@ type library_disk = {
   md_imports : compilation_unit_name array }
 
 type opaque_table = constr Future.computation array
-type univ_table = Univ.constraints Future.computation array option
+type univ_table =
+  (Univ.constraints Future.computation array * Univ.constraints * bool) option
 
 (** A .vo file is currently made of :
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 1485d6bf0..be6bdec11 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -22,7 +22,7 @@ type env = {
     env_globals       : globals;
     env_rel_context   : rel_context;
     env_stratification : stratification;
-    env_imports : Digest.t MPmap.t }
+    env_imports : Cic.vodigest MPmap.t }
 
 let empty_env = {
   env_globals =
diff --git a/checker/environ.mli b/checker/environ.mli
index a4162d67f..46b390d0a 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -17,7 +17,7 @@ type env = {
   env_globals : globals;
   env_rel_context : rel_context;
   env_stratification : stratification;
-  env_imports : Digest.t MPmap.t;
+  env_imports : Cic.vodigest MPmap.t;
 }
 val empty_env : env
 
@@ -26,8 +26,8 @@ val engagement : env -> Cic.engagement option
 val set_engagement : Cic.engagement -> env -> env
 
 (* Digests *)
-val add_digest : env -> DirPath.t -> Digest.t -> env
-val lookup_digest : env -> DirPath.t -> Digest.t
+val add_digest : env -> DirPath.t -> Cic.vodigest -> env
+val lookup_digest : env -> DirPath.t -> Cic.vodigest
 
 (* de Bruijn variables *)
 val rel_context : env -> rel_context
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ec0014175..add993581 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,9 +26,6 @@ let refresh_arity ar =
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
 (*  let env = add_constraints cb.const_constraints env in*)
-  (* Constraints of an opauqe proof are not in the module *)
-  let env =
-    add_constraints (Declarations.force_lazy_constr_univs cb.const_body) env in
   (match cb.const_type with
       NonPolymorphicType ty ->
         let ty, cu = refresh_arity ty in
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7fcd749f5..0d7364ce6 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -25,9 +25,10 @@ let set_engagement c =
   genv := set_engagement c !genv
 
 (* full_add_module adds module with universes and constraints *)
-let full_add_module dp mb digest =
+let full_add_module dp mb univs digest =
   let env = !genv in
   let env = add_constraints mb.mod_constraints env in
+  let env = add_constraints univs env in
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
@@ -68,19 +69,20 @@ let stamp_library file digest = ()
 
 (* When the module is checked, digests do not need to match, but a
    warning is issued in case of mismatch *)
-let import file clib digest =
+let import file clib univs digest =
   let env = !genv in
   check_imports msg_warning clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
-    (add_constraints mb.mod_constraints env) mb.mod_mp mb;
+    (add_constraints univs
+      (add_constraints mb.mod_constraints env)) mb.mod_mp mb;
   stamp_library file digest;
-  full_add_module clib.comp_name mb digest
+  full_add_module clib.comp_name mb univs digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file clib digest =
+let unsafe_import file clib univs digest =
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
-  full_add_module clib.comp_name clib.comp_mod digest
+  full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 59d95c36d..e2aad1d93 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -15,6 +15,6 @@ val get_env : unit -> env
 
 val set_engagement : engagement -> unit
 val import         :
-  CUnix.physical_path -> compiled_library -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
 val unsafe_import  :
-  CUnix.physical_path -> compiled_library -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 0a2e53799..f73f83d16 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -284,7 +284,8 @@ and v_modtype =
 
 (** kernel/safe_typing *)
 
-let v_deps = Array (v_tuple "dep" [|v_dp;String|])
+let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
+let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
   v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
 
@@ -301,7 +302,8 @@ let v_lib =
   Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
 
 let v_opaques = Array (v_computation v_constr)
-let v_univopaques = Opt (Array (v_computation v_cstrs))
+let v_univopaques =
+  Opt (Tuple ("univopaques",[|Array (v_computation v_cstrs);v_cstrs;v_bool|]))
 
 (** Registering dynamic values *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 867705c47..8ff01a755 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -91,7 +91,18 @@ open Declarations
 
 *)
 
-type library_info = DirPath.t * Digest.t
+type vodigest =
+  | Dvo_or_vi of Digest.t        (* The digest of the seg_lib part *)
+  | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+let digest_match ~actual ~required =
+  match actual, required with
+  | Dvo_or_vi d1, Dvo_or_vi d2
+  | Dvivo (d1,_), Dvo_or_vi d2 -> String.equal d1 d2
+  | Dvivo (d1,e1), Dvivo (d2,e2) -> String.equal d1 d2 && String.equal e1 e2
+  | Dvo_or_vi _, Dvivo _ -> false
+
+type library_info = DirPath.t * vodigest
 
 (** Functor and funsig parameters, most recent first *)
 type module_parameters = (MBId.t * module_type_body) list
@@ -252,11 +263,11 @@ let check_initial senv = assert (is_initial senv)
     with the correct digests. *)
 
 let check_imports current_libs needed =
-  let check (id,stamp) =
+  let check (id,required) =
     try
-      let actual_stamp = List.assoc_f DirPath.equal id current_libs in
-      if not (String.equal stamp actual_stamp) then
-	Errors.error
+      let actual = List.assoc_f DirPath.equal id current_libs in
+      if not(digest_match ~actual ~required) then
+        Errors.error
           ("Inconsistent assumptions over module "^(DirPath.to_string id)^".")
     with Not_found ->
       Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".")
@@ -661,8 +672,6 @@ type compiled_library = {
 
 type native_library = Nativecode.global list
 
-let join_compiled_library l = Modops.join_module l.comp_mod
-
 let start_library dir senv =
   check_initial senv;
   assert (not (DirPath.is_empty dir));
@@ -709,12 +718,15 @@ let export compilation_mode senv dir =
   in
   mp, lib, ast
 
-let import lib digest senv =
+(* cst are the constraints that were computed by the vi2vo step and hence are
+ * not part of the mb.mod_constraints field (but morally should be) *)
+let import lib cst vodigest senv =
   check_imports senv.imports lib.comp_deps;
   check_engagement senv.env lib.comp_enga;
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
   let env = Environ.add_constraints mb.mod_constraints senv.env in
+  let env = Environ.add_constraints cst env in
   (mp, lib.comp_natsymbs),
   { senv with
     env =
@@ -723,10 +735,9 @@ let import lib digest senv =
        in
        Modops.add_linked_module mb linkinfo env);
     modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
-    imports = (lib.comp_name,digest)::senv.imports;
+    imports = (lib.comp_name,vodigest)::senv.imports;
     loads = (mp,mb)::senv.loads }
 
-
 (** {6 Safe typing } *)
 
 type judgment = Environ.unsafe_judgment
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e2d1e37e9..d70d7d8be 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -8,6 +8,12 @@
 
 open Names
 
+type vodigest =
+  | Dvo_or_vi of Digest.t        (* The digest of the seg_lib part *)
+  | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+val digest_match : actual:vodigest -> required:vodigest -> bool
+
 (** {6 Safe environments } *)
 
 (** Since we are now able to type terms, we can define an abstract type
@@ -120,11 +126,10 @@ val export :
   safe_environment -> DirPath.t ->
     module_path * compiled_library * native_library
 
-val import : compiled_library -> Digest.t ->
+(* Constraints are non empty iff the file is a vi2vo *)
+val import : compiled_library -> Univ.constraints -> vodigest ->
   (module_path * Nativecode.symbol array) safe_transformer
 
-val join_compiled_library : compiled_library -> unit
-
 (** {6 Safe typing judgments } *)
 
 type judgment
diff --git a/library/declaremods.ml b/library/declaremods.ml
index c60e008d1..2b917587c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -849,7 +849,7 @@ type library_values = Nativecode.symbol array
 let library_values =
   Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES"
 
-let register_library dir cenv (objs:library_objects) digest =
+let register_library dir cenv (objs:library_objects) digest univ =
   let mp = MPfile dir in
   let () =
     try
@@ -857,7 +857,7 @@ let register_library dir cenv (objs:library_objects) digest =
       ignore(Global.lookup_module mp);
     with Not_found ->
       (* If not, let's do it now ... *)
-      let mp', values = Global.import cenv digest in
+      let mp', values = Global.import cenv univ digest in
       if not (ModPath.equal mp mp') then
         anomaly (Pp.str "Unexpected disk module name");
       library_values := Dirmap.add dir values !library_values
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
 
diff --git a/library/global.ml b/library/global.ml
index 9515ff1a8..f75c8e592 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -129,7 +129,7 @@ let mind_of_delta_kn kn =
 
 let start_library dir = globalize (Safe_typing.start_library dir)
 let export s = Safe_typing.export !Flags.compilation_mode (safe_env ()) s
-let import cenv digest = globalize (Safe_typing.import cenv digest)
+let import c u d = globalize (Safe_typing.import c u d)
 
 
 (** Function to get an environment from the constants part of the global
diff --git a/library/global.mli b/library/global.mli
index 856956a17..e11e1c017 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -85,7 +85,8 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive
 val start_library : DirPath.t -> module_path
 val export : DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
-val import : Safe_typing.compiled_library -> Digest.t ->
+val import :
+  Safe_typing.compiled_library -> Univ.constraints -> Safe_typing.vodigest ->
   module_path * Nativecode.symbol array
 
 (** {6 Misc } *)
diff --git a/library/library.ml b/library/library.ml
index a1760cdf1..b75329a22 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -26,7 +26,7 @@ type library_disk = {
   md_name : compilation_unit_name;
   md_compiled : Safe_typing.compiled_library;
   md_objects : Declaremods.library_objects;
-  md_deps : (compilation_unit_name * Digest.t) array;
+  md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   md_imports : compilation_unit_name array }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -36,9 +36,11 @@ type library_t = {
   library_name : compilation_unit_name;
   library_compiled : Safe_typing.compiled_library;
   library_objects : Declaremods.library_objects;
-  library_deps : (compilation_unit_name * Digest.t) array;
+  library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
-  library_digest : Digest.t }
+  library_digests : Safe_typing.vodigest;
+  library_extra_univs : Univ.constraints;
+}
 
 module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
@@ -441,32 +443,40 @@ let () =
 (* Internalise libraries *)
 
 type seg_lib = library_disk
-type seg_univ = Univ.constraints Future.computation array
+type seg_univ = (* true = vivo, false = vi *)
+  Univ.constraints Future.computation array * Univ.constraints * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
-let mk_library md digest =
+let mk_library md digests univs =
   {
     library_name     = md.md_name;
     library_compiled = md.md_compiled;
     library_objects  = md.md_objects;
     library_deps     = md.md_deps;
     library_imports  = md.md_imports;
-    library_digest    = digest
+    library_digests  = digests;
+    library_extra_univs = univs;
   }
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
   let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
-  let (univs : seg_univ option), _, _ = System.marshal_in_segment f ch in
-  Option.iter (fun univs -> add_univ_table lmd.md_name (Fetched univs)) univs;
+  let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
   let pos, digest = System.skip_in_segment f ch in
+  close_in ch;
   register_library_filename lmd.md_name f;
   add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
-  let library = mk_library lmd digest_lmd in
-  close_in ch;
-  library
+  let open Safe_typing in
+  match univs with
+  | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint
+  | Some (utab,uall,true) ->
+      add_univ_table lmd.md_name (Fetched utab);
+      mk_library lmd (Dvivo (digest_lmd,digest_u)) uall
+  | Some (utab,_,false) ->
+      add_univ_table lmd.md_name (Fetched utab);
+      mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint
 
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
@@ -489,10 +499,10 @@ and intern_library_deps needed dir m =
 
 and intern_mandatory_library caller needed (dir,d) =
   let m,needed = intern_library needed (try_locate_absolute_library dir) in
-  if not (String.equal d m.library_digest) then
-    errorlabstrm "" (strbrk ("Compiled library "^(DirPath.to_string caller)^
-	   ".vo makes inconsistent assumptions over library "
-	   ^(DirPath.to_string dir)));
+  if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then
+    errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
+      ".vo makes inconsistent assumptions over library " ^
+      DirPath.to_string dir));
   needed
 
 let rec_intern_library needed mref =
@@ -553,7 +563,8 @@ let register_library m =
     m.library_name
     m.library_compiled
     m.library_objects
-    m.library_digest;
+    m.library_digests
+    m.library_extra_univs;
   register_loaded_library m
 
 (* Follow the semantics of Anticipate object:
@@ -686,13 +697,14 @@ let load_library_todo f =
   if tasks = None then errorlabstrm "restart" (str"not a .vi file");
   if s2 = None then errorlabstrm "restart" (str"not a .vi file");
   if s3 = None then errorlabstrm "restart" (str"not a .vi file");
+  if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vi file");
   longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
 
 let current_deps () =
-  List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list
+  List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list
 
 let current_reexports () =
   List.map (fun m -> m.library_name) !libraries_exports_list
@@ -722,7 +734,8 @@ let save_library_to ?todo dir f =
         f ^ "o", (fun _ -> None), (fun _ -> None), (fun _ -> None)
     | Some d ->
         assert(!Flags.compilation_mode = Flags.BuildVi);
-        f ^ "i", (fun x -> Some (d x)), (fun x -> Some x), (fun x -> Some x) in
+        f ^ "i", (fun x -> Some (d x)),
+          (fun x -> Some (x,Univ.empty_constraint,false)), (fun x -> Some x) in
   Opaqueproof.reset_indirect_creator ();
   (* HACK: end_library resets Lib and then joins the safe env.  To join the
    * env one needs to access the futures stored in the tables.  Standard
diff --git a/library/library.mli b/library/library.mli
index afcce7f6c..16664d880 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -30,7 +30,8 @@ val require_library_from_file :
 
 (** Segments of a library *)
 type seg_lib
-type seg_univ = Univ.constraints Future.computation array
+type seg_univ = (* cst, all_cst, finished? *)
+  Univ.constraints Future.computation array * Univ.constraints * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 8c1c6b02b..9cb5e9511 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -641,7 +641,7 @@ module Slaves : sig
   val finish_task :
     string ->
     Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
-    tasks -> int -> unit
+    tasks -> int -> Library.seg_univ
 
   val cancel_worker : int -> unit
 
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
           Pp.msg_error (str"unable to print error message: " ++
                         str (Printexc.to_string e))); None
 
-  let finish_task name u d p l i =
+  let finish_task name (u,cst,_) d p l i =
     let bucket =
       match List.nth l i with ReqBuildProof (_,_,_,_,bucket,_) -> bucket in
     match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
@@ -898,9 +898,10 @@ end = struct (* {{{ *)
             let pr = Future.chain ~greedy:true ~pure:true pr discharge in
             let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
             Future.sink pr;
-            Future.sink uc;
+            let extra = Future.join uc in
             u.(bucket) <- uc;
-            p.(bucket) <- pr
+            p.(bucket) <- pr;
+            u, Univ.union_constraints cst extra, false
         | _ -> assert false
   
   let check_task name l i =
@@ -1611,12 +1612,15 @@ let check_task name (tasks,_) i =
 let info_tasks (tasks,_) = Slaves.info_tasks tasks
 let finish_tasks name u d p (t,rcbackup as tasks) =
   RemoteCounter.restore rcbackup;
-  let finish_task (_,_,i) =
+  let finish_task u (_,_,i) =
     let vcs = VCS.backup () in
-    Future.purify (Slaves.finish_task name u d p t) i;
+    let u = Future.purify (Slaves.finish_task name u d p t) i in
     Pp.pperr_flush ();
-    VCS.restore vcs in
-  try List.iter finish_task (info_tasks tasks)
+    VCS.restore vcs;
+    u in
+  try
+    let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
+    (u,a,true), p
   with e ->
     Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e);
     exit 1
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index c47bacf65..1eba274ab 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -50,7 +50,7 @@ val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list
 val finish_tasks : string ->
   Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
-  tasks -> unit
+  tasks -> Library.seg_univ * Library.seg_proofs
 
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4ea9c2236..11cb726c7 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -348,6 +348,6 @@ let compile verbosely f =
       let f = if check_suffix f ".vi" then chop_extension f else f in
       let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
       Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv);
-      Stm.finish_tasks lfdv univs disch proofs tasks;
+      let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv lib univs proofs