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).

3 files changed, 14 insertions, 10 deletions

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