New compilation mode -vi2vo

To obtain a.vo one can now:
1) coqtop -quick -compile a
2) coqtop -vi2vo a.vi

To make that possible the .vo structure has been complicated.  It is now
made of 5 segments.

               |  vo  | vi  | vi2vo | contents
 --------------+------+-----+-------+------------------------------------
 lib           | Yes  | Yes | Yes   | libstack (modules, notations,...)
 opauqe_univs  | No   | Yes | Yes   | constraints coming from opaque proofs
 discharge     | No   | Yes | No    | data needed to close sections
 tasks         | No   | Yes | No    | STM tasks to produce proof terms
 opaque_proofs | Yes  | Yes | Yes   | proof terms
 --------------+------+-----+-------+------------------------------------

This means one can load only the strictly necessay parts.  Usually one
does not load the tasks segment of a .vi nor the opaque_proof segment of
a .vo, unless one is turning a .vi into a .vo, in which case he load
all the segments.

Optional segments are marshalled as None.  But for lib, all segments
are Array.t of:

               | type
 --------------+---------------------------------------------------------
 lib           | a list of Libobject.obj (n'importe quoi)
 opauqe_univs  | Univ.consraints Future.computation
 discharge     | what Cooking.cook_constr needs
 tasks         | Stm.tasks (a task is system_state * vernacexpr list)
 opaque_proofs | Term.constr Future.computation
 --------------+------+-----+-------+------------------------------------

Invariant: all Future.computation in a vo file (obtained by a vi2vo
compilation or not) have been terminated with Future.join (or
Future.sink).  This means they are values (inside a box).
This invariant does not hold for vi files.  E.g. opauqe_proofs can be
dangling Future.computation (i.e. NotHere exception).  The vi2vo
compilation step will replace them by true values.

Rationale for opaque_univs: in the vi2vo transformation we want to reuse
the lib segment.  Hence the missing pieces have to be put on the side,
not inside.  Opaque proof terms are already in a separte segment.
Universe constraints are not, hence the new opauqe_univs segment.  Such
segment, if present in a .vo file, is always loaded, and
Declare.open_constant will add to the environment the constraints stored
there.  For regular constants this is not necessay since the constraints
are already in their enclosing module (and also in the constant_body).
With vi2vo the constraints coming from the proof are not in the
constant_body (hence not in the enclosing module) but there and are
added to the environment explicitly by Declare.open_constant.

Rationale for discharge: vi2vo produces a proof term in its original
context (in the middle of a section).  Then it has to discharge the
object.  This segment contains the data that is needed in order to do
so.  It is morally the input that Lib.close_section passes to Cooking
(via the insane rewinding of libstack, GlobalRecipe, etc chain).

Checksums: the checksum of .vi and a .vo obtain from it is the same.
This means that if if b.vo has been compiled using a.vi, and then
a.vi is compiled into a.vo, Require Import b works (and recursively
loads a.vo).

28 files changed, 481 insertions, 225 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0a1d713c4..75642648d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -23,8 +23,6 @@ open Environ
 
 (*s Cooking the constants. *)
 
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-
 let pop_dirpath p = match DirPath.repr p with
   | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath")
   | _::l -> DirPath.make l
@@ -111,35 +109,34 @@ let abstract_constant_type =
 let abstract_constant_body =
   List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
 
-type recipe = {
-  d_from : constant_body;
-  d_abstract : named_context;
-  d_modlist : work_list }
-
+type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
 type inline = bool
 
 type result =
-  constant_def * constant_type * constant_constraints * inline
+  constant_def * constant_type * Univ.constraints * inline
     * Context.section_context option
 
-let on_body f = function
+let on_body ml hy f = function
   | Undef _ as x -> x
   | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
   | OpaqueDef lc ->
-    OpaqueDef (Future.chain ~pure:true lc (fun lc ->
-        (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))))
+    OpaqueDef (Lazyconstr.discharge_direct_lazy_constr ml hy f lc)
 
 let constr_of_def = function
   | Undef _ -> assert false
   | Def cs -> Lazyconstr.force cs
-  | OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc)
+  | OpaqueDef lc -> Lazyconstr.force_opaque lc
+
+let cook_constr { Lazyconstr.modlist ; abstract } c =
+  let cache = Hashtbl.create 13 in
+  let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
+  abstract_constant_body (expmod_constr cache modlist c) hyps
 
-let cook_constant env r =
+let cook_constant env { from = cb; info = { Lazyconstr.modlist; abstract } } =
   let cache = Hashtbl.create 13 in
-  let cb = r.d_from in
-  let hyps = Context.map_named_context (expmod_constr cache r.d_modlist) r.d_abstract in
-  let body = on_body
-    (fun c -> abstract_constant_body (expmod_constr cache r.d_modlist c) hyps)
+  let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
+  let body = on_body modlist hyps
+    (fun c -> abstract_constant_body (expmod_constr cache modlist c) hyps)
     cb.const_body
   in
   let const_hyps =
@@ -149,12 +146,12 @@ let cook_constant env r =
   let typ = match cb.const_type with
     | NonPolymorphicType t ->
 	let typ =
-          abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in
+          abstract_constant_type (expmod_constr cache modlist t) hyps in
 	NonPolymorphicType typ
     | PolymorphicArity (ctx,s) ->
 	let t = mkArity (ctx,Type s.poly_level) in
 	let typ =
-          abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in
+          abstract_constant_type (expmod_constr cache modlist t) hyps in
 	let j = make_judge (constr_of_def body) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 2d6e53407..05c7a2040 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -14,22 +14,18 @@ open Univ
 
 (** {6 Cooking the constants. } *)
 
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-
-type recipe = {
-  d_from : constant_body;
-  d_abstract : Context.named_context;
-  d_modlist : work_list }
+type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
 
 type inline = bool
 
 type result =
-  constant_def * constant_type * constant_constraints * inline
+  constant_def * constant_type * Univ.constraints * inline
     * Context.section_context option
 
 val cook_constant : env -> recipe -> result
+val cook_constr : Lazyconstr.cooking_info -> Term.constr -> Term.constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
 
-val expmod_constr : work_list -> constr -> constr
+val expmod_constr : Lazyconstr.work_list -> constr -> constr
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d92b66707..ef56ae512 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -38,16 +38,16 @@ type inline = int option
 type constant_def =
   | Undef of inline
   | Def of Lazyconstr.constr_substituted
-  | OpaqueDef of Lazyconstr.lazy_constr Future.computation
-
-type constant_constraints = Univ.constraints Future.computation
+  | OpaqueDef of Lazyconstr.lazy_constr
 
+(* some contraints are in constant_constraints, some other may be in
+ * the OpaueDef *)
 type constant_body = {
     const_hyps : Context.section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
-    const_constraints : constant_constraints;
+    const_constraints : Univ.constraints;
     const_inline_code : bool }
 
 type side_effect =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index e40441d74..21a961fc3 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,7 +19,13 @@ open Util
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
   | Def c -> Some (Lazyconstr.force c)
-  | OpaqueDef lc -> Some (Lazyconstr.force_opaque (Future.force lc))
+  | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
+
+let constraints_of_constant cb = Univ.union_constraints cb.const_constraints
+ (match cb.const_body with
+  | Undef _ -> Univ.empty_constraint
+  | Def c -> Univ.empty_constraint
+  | OpaqueDef lc -> snd (Lazyconstr.force_opaque_w_constraints lc))
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
@@ -52,8 +58,7 @@ let subst_const_type sub arity = match arity with
 let subst_const_def sub def = match def with
   | Undef _ -> def
   | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc ->
-      OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
+  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
 
 let subst_const_body sub cb =
   assert (List.is_empty cb.const_hyps); (* we're outside sections *)
@@ -101,20 +106,13 @@ let hcons_const_def = function
   | Def l_constr ->
     let constr = force l_constr in
     Def (from_val (Term.hcons_constr constr))
-  | OpaqueDef lc ->
-    OpaqueDef
-      (Future.chain ~greedy:true ~pure:true lc
-         (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc))))
+  | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
 
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = hcons_const_type cb.const_type;
-    const_constraints =
-      if Future.is_val cb.const_constraints then
-        Future.from_val
-          (Univ.hcons_constraints (Future.force cb.const_constraints))
-      else cb.const_constraints }
+    const_constraints = Univ.hcons_constraints cb.const_constraints; }
 
 (** {6 Inductive types } *)
 
@@ -239,9 +237,8 @@ let hcons_mind mib =
 (** {6 Stm machinery } *)
 
 let join_constant_body cb =
-  ignore(Future.join cb.const_constraints);
   match cb.const_body with
-  | OpaqueDef d -> ignore(Future.join d)
+  | OpaqueDef d -> Lazyconstr.join_lazy_constr d
   | _ -> ()
 
 let string_of_side_effect = function
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 177ae9d45..800b167ab 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -24,6 +24,7 @@ val constant_has_body : constant_body -> bool
     Only use this function if you know what you're doing. *)
 
 val body_of_constant : constant_body -> Term.constr option
+val constraints_of_constant : constant_body -> Univ.constraints
 
 val is_opaque : constant_body -> bool
 
diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
index 21aba6348..23d6d559d 100644
--- a/kernel/lazyconstr.ml
+++ b/kernel/lazyconstr.ml
@@ -10,6 +10,9 @@ open Names
 open Term
 open Mod_subst
 
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context } 
+
 (** [constr_substituted] are [constr] with possibly pending
     substitutions of kernel names. *)
 
@@ -29,48 +32,103 @@ let subst_constr_subst = subst_substituted
     should end in a .vo, this is checked by coqchk.
 *)
 
+type proofterm = (constr * Univ.constraints) Future.computation
 type lazy_constr =
-  | Indirect of substitution list * DirPath.t * int (* lib,index *)
-  | Direct of constr_substituted (* opaque in section or interactive session *)
+  (* subst, lib, index *)
+  | Indirect of substitution list * DirPath.t * int
+  (* opaque in section or interactive session *)
+  | Direct of cooking_info list * (constr_substituted * Univ.constraints) Future.computation
 
 (* TODO : this hcons function could probably be improved (for instance
    hash the dir_path in the Indirect case) *)
 
-let hcons_lazy_constr = function
-  | Direct c -> Direct (from_val (hcons_constr (force c)))
-  | Indirect _ as lc -> lc
-
 let subst_lazy_constr sub = function
-  | Direct cs -> Direct (subst_constr_subst sub cs)
+  | Direct ([],cu) ->
+      Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
+        subst_constr_subst sub c, u))
+  | Direct _ -> Errors.anomaly (Pp.str"still direct but not discharged")
   | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
 
+let iter_direct_lazy_constr f = function
+  | Indirect _ -> Errors.anomaly (Pp.str "iter_direct_lazy_constr")
+  | Direct (d,cu) ->
+      Direct (d, Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> f (force c); c, u))
+
+let discharge_direct_lazy_constr modlist abstract  f = function
+  | Indirect _ -> Errors.anomaly (Pp.str "discharge_direct_lazy_constr")
+  | Direct (d,cu) ->
+      Direct ({ modlist; abstract }::d,
+        Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
+          from_val (f (force c)), u))
+
 let default_get_opaque dp _ =
   Errors.error
-    ("Cannot access an opaque term in library " ^ DirPath.to_string dp)
+    ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
+let default_get_univ dp _ =
+  Errors.error
+    ("Cannot access universe constraints of opaque proofs in library " ^
+    DirPath.to_string dp)
 
-let default_mk_opaque _ = None
+let default_mk_indirect _ = None
+
+let default_join_indirect_local_opaque _ _ = ()
+let default_join_indirect_local_univ _ _ = ()
 
 let get_opaque = ref default_get_opaque
-let mk_opaque = ref default_mk_opaque
+let get_univ = ref default_get_univ
+let join_indirect_local_opaque = ref default_join_indirect_local_opaque
+let join_indirect_local_univ = ref default_join_indirect_local_univ
+
+let mk_indirect = ref default_mk_indirect
 let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_opaque_creator f = (mk_opaque := f)
-let reset_indirect_opaque_creator () = (mk_opaque := default_mk_opaque)
+let set_indirect_univ_accessor f = (get_univ := f)
+let set_indirect_creator f = (mk_indirect := f)
+let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
+let set_join_indirect_local_univ f = join_indirect_local_univ := f
+
+let reset_indirect_creator () = mk_indirect := default_mk_indirect
 
 let force_lazy_constr = function
-  | Direct c -> c
+  | Direct (_,c) -> Future.force c
   | Indirect (l,dp,i) ->
-    List.fold_right subst_constr_subst l (from_val (!get_opaque dp i))
+      let c = Future.force (!get_opaque dp i) in
+      List.fold_right subst_constr_subst l (from_val c),
+      Future.force
+        (Option.default
+          (Future.from_val Univ.empty_constraint)
+          (!get_univ dp i))
+
+let join_lazy_constr = function
+  | Direct (_,c) -> ignore(Future.force c)
+  | Indirect (_,dp,i) ->
+      !join_indirect_local_opaque dp i;
+      !join_indirect_local_univ dp i
 
 let turn_indirect lc = match lc with
   | Indirect _ ->
     Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
-  | Direct c ->
-    (* this constr_substituted shouldn't have been substituted yet *)
-    assert (fst (Mod_subst.repr_substituted c) == None);
-    match !mk_opaque (force c) with
+  | Direct (d,cu) ->
+    let cu = Future.chain ~greedy:true ~pure:true cu (fun (c,u) ->
+      (* this constr_substituted shouldn't have been substituted yet *)
+      assert (fst (Mod_subst.repr_substituted c) == None);
+      hcons_constr (force c),u) in
+    match !mk_indirect (d,cu) with
       | None -> lc
       | Some (dp,i) -> Indirect ([],dp,i)
 
-let force_opaque lc = force (force_lazy_constr lc)
-
-let opaque_from_val c = Direct (from_val c)
+let force_opaque lc =
+  let c, _u = force_lazy_constr lc in force c
+let force_opaque_w_constraints lc =
+  let c, u = force_lazy_constr lc in force c, u
+let get_opaque_future_constraints lc = match lc with
+  | Indirect (_,dp,i) -> !get_univ dp i
+  | Direct (_,cu) -> Some(snd (Future.split2 ~greedy:true cu))
+let get_opaque_futures lc = match lc with
+  | Indirect _ -> assert false
+  | Direct (_,cu) ->
+      let cu =
+        Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> force c, u) in
+      Future.split2 ~greedy:true cu
+
+let opaque_from_val cu =
+  Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> from_val c, u))
diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli
index f6188f536..db4d8fb72 100644
--- a/kernel/lazyconstr.mli
+++ b/kernel/lazyconstr.mli
@@ -10,6 +10,9 @@ open Names
 open Term
 open Mod_subst
 
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context } 
+
 (** [constr_substituted] are [constr] with possibly pending
     substitutions of kernel names. *)
 
@@ -25,9 +28,10 @@ val subst_constr_subst :
     this might trigger the read of some extra parts of .vo files *)
 
 type lazy_constr
+type proofterm = (constr * Univ.constraints) Future.computation
 
 (** From a [constr] to some (immediate) [lazy_constr]. *)
-val opaque_from_val : constr -> lazy_constr
+val opaque_from_val : proofterm -> lazy_constr
 
 (** Turn an immediate [lazy_constr] into an indirect one, thanks
     to the indirect opaque creator configured below. *)
@@ -36,10 +40,22 @@ val turn_indirect : lazy_constr -> lazy_constr
 (** From a [lazy_constr] back to a [constr]. This might use the
     indirect opaque accessor configured below. *)
 val force_opaque : lazy_constr -> constr
+val force_opaque_w_constraints : lazy_constr -> constr * Univ.constraints
+val get_opaque_future_constraints :
+  lazy_constr -> Univ.constraints Future.computation option
+val get_opaque_futures :
+  lazy_constr ->
+    Term.constr Future.computation * Univ.constraints Future.computation
 
 val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
 
-val hcons_lazy_constr : lazy_constr -> lazy_constr
+(* val hcons_lazy_constr : lazy_constr -> lazy_constr *)
+
+(* Used to discharge the proof term. *)
+val iter_direct_lazy_constr : (constr -> unit) -> lazy_constr -> lazy_constr
+val discharge_direct_lazy_constr : work_list -> Context.named_context -> (constr -> constr) -> lazy_constr -> lazy_constr
+
+val join_lazy_constr : lazy_constr -> unit
 
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The following two functions activate
@@ -48,6 +64,12 @@ val hcons_lazy_constr : lazy_constr -> lazy_constr
     any indirect link, and default accessor always raises an error.
 *)
 
-val set_indirect_opaque_creator : (constr -> (DirPath.t * int) option) -> unit
-val set_indirect_opaque_accessor : (DirPath.t -> int -> constr) -> unit
-val reset_indirect_opaque_creator : unit -> unit
+val set_indirect_creator :
+  (cooking_info list * proofterm -> (DirPath.t * int) option) -> unit
+val set_indirect_opaque_accessor :
+  (DirPath.t -> int -> Term.constr Future.computation) -> unit
+val set_indirect_univ_accessor :
+  (DirPath.t -> int -> Univ.constraints Future.computation option) -> unit
+val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit
+val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit
+val reset_indirect_creator : unit -> unit
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 7794f19be..6e656fad9 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -77,11 +77,11 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	  let j,cst1 = Typeops.infer env' c in
 	  let typ = Typeops.type_of_constant_type env' cb.const_type in
 	  let cst2 = Reduction.conv_leq env' j.uj_type typ in
-	  let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in
-	  j.uj_val,cst
+	  let cst = cb.const_constraints +++ cst1 +++ cst2 in
+	  j.uj_val, cst
 	| Def cs ->
 	  let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
-	  let cst = Future.force cb.const_constraints +++ cst1 in
+	  let cst = cb.const_constraints +++ cst1 in
           c, cst
       in
       let def = Def (Lazyconstr.from_val c') in
@@ -89,7 +89,7 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	{ cb with
 	  const_body = def;
 	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
-	  const_constraints = Future.from_val cst }
+	  const_constraints = cst }
       in
       before@(lab,SFBconst(cb'))::after, c', cst
     else
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3e9b646c1..a93415f92 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -282,11 +282,11 @@ let safe_push_named (id,_,_ as d) env =
 
 let push_named_def (id,de) senv =
   let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
-  let c = match c with
-    | Def c -> Lazyconstr.force c
-    | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c)
+  let c,cst' = match c with
+    | Def c -> Lazyconstr.force c, Univ.empty_constraint
+    | OpaqueDef c -> Lazyconstr.force_opaque_w_constraints c
     | _ -> assert false in
-  let cst = Future.join cst in
+  let senv = add_constraints (Now cst') senv in
   let senv' = add_constraints (Now cst) senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
   (cst, {senv' with env=env''})
@@ -314,13 +314,19 @@ let labels_of_mib mib =
   get ()
 
 let constraints_of_sfb = function
-  | SFBmind mib -> Now mib.mind_constraints
-  | SFBmodtype mtb -> Now mtb.typ_constraints
-  | SFBmodule mb -> Now mb.mod_constraints
-  | SFBconst cb ->
-      match Future.peek_val cb.const_constraints with
-      | Some c -> Now c
-      | None -> Later cb.const_constraints
+  | SFBmind mib -> [Now mib.mind_constraints]
+  | SFBmodtype mtb -> [Now mtb.typ_constraints]
+  | SFBmodule mb -> [Now mb.mod_constraints]
+  | SFBconst cb -> [Now cb.const_constraints] @
+      match cb.const_body with
+      | (Undef _ | Def _) -> []
+      | OpaqueDef lc ->
+          match Lazyconstr.get_opaque_future_constraints lc with
+          | None -> []
+          | Some fc ->
+              match Future.peek_val fc with
+              | None -> [Later fc]
+              | Some c -> [Now c]
 
 (** A generic function for adding a new field in a same environment.
     It also performs the corresponding [add_constraints]. *)
@@ -341,7 +347,7 @@ let add_field ((l,sfb) as field) gn senv =
     | SFBmodule _ | SFBmodtype _ ->
       check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
-  let senv = add_constraints (constraints_of_sfb sfb) senv in
+  let senv = List.fold_right add_constraints (constraints_of_sfb sfb) senv in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
     | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -377,8 +383,7 @@ let add_constant dir l decl senv =
     | OpaqueDef lc when DirPath.is_empty dir ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
-      { cb with const_body =
-           OpaqueDef (Future.chain ~greedy:true ~pure:true lc Lazyconstr.turn_indirect) }
+      { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
     | _ -> cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
@@ -660,10 +665,11 @@ let start_library dir senv =
 let export compilation_mode senv dir =
   let senv =
     try
-      if compilation_mode = Flags.BuildVi then senv (* FIXME: cleanup future*)
+      if compilation_mode = Flags.BuildVi then { senv with future_cst = [] }
       else join_safe_environment senv
-    with e -> Errors.errorlabstrm "future" (Errors.print e)
+    with e -> Errors.errorlabstrm "export" (Errors.print e)
   in
+  assert(senv.future_cst = []);
   let () = check_current_library dir senv in
   let mp = senv.modpath in
   let str = NoFunctor (List.rev senv.revstruct) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 55901bce9..f059ea1ae 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -28,15 +28,21 @@ let prerr_endline =
   if debug then prerr_endline else fun _ -> ()
 
 let constrain_type env j cst1 = function
-  | None ->
+  | `None ->
       make_polymorphic_if_constant_for_ind env j, cst1
-  | Some t ->
+  | `Some t ->
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
       assert (eq_constr t tj.utj_val);
       let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
       NonPolymorphicType t, cstrs
+  | `SomeWJ (t, tj, cst2) ->
+      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
+      assert (eq_constr t tj.utj_val);
+      let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
+      NonPolymorphicType t, cstrs
 
+let map_option_typ = function None -> `None | Some x -> `Some x
 
 let translate_local_assum env t =
   let (j,cst) = infer env t in
@@ -68,7 +74,7 @@ let handle_side_effects env body side_eff =
           let t = sub c 1 (Vars.lift 1 t) in
           mkLetIn (cname c, b, b_ty, t)
       | OpaqueDef b -> 
-          let b = Lazyconstr.force_opaque (Future.join b) in
+          let b = Lazyconstr.force_opaque b in
           let b_ty = Typeops.type_of_constant_type env cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
@@ -84,28 +90,27 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete)
   
-(* what is used for debugging only *)
-let infer_declaration ?(what="UNKNOWN") env dcl =
+let infer_declaration env dcl =
   match dcl with
   | ParameterEntry (ctx,t,nl) ->
       let j, cst = infer env t in
       let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx
+      Undef nl, NonPolymorphicType t, cst, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true } as c) ->
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
-      let body_cst =
+      let tyj, tycst = infer_type env typ in
+      let proofterm =
         Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
           let body = handle_side_effects env body side_eff in
           let j, cst = infer env body in
           let j = hcons_j j in
-          let _typ, cst = constrain_type env j cst (Some typ) in
+          let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in
           feedback_completion_typecheck feedback_id;
-          Lazyconstr.opaque_from_val j.uj_val, cst) in
-      let body, cst = Future.split2 ~greedy:true body_cst in
-      let def = OpaqueDef body in
+          j.uj_val, cst) in
+      let def = OpaqueDef (Lazyconstr.opaque_from_val proofterm) in
       let typ = NonPolymorphicType typ in
-      def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+      def, typ, tycst, c.const_entry_inline_code, c.const_entry_secctx
   | DefinitionEntry c ->
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
@@ -113,10 +118,9 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
       let body = handle_side_effects env body side_eff in
       let j, cst = infer env body in
       let j = hcons_j j in
-      let typ, cst = constrain_type env j cst typ in
+      let typ, cst = constrain_type env j cst (map_option_typ typ) in
       feedback_completion_typecheck feedback_id;
       let def = Def (Lazyconstr.from_val j.uj_val) in
-      let cst = Future.from_val cst in
       def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
 
 let global_vars_set_constant_type env = function
@@ -127,7 +131,6 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-
 let record_aux env s1 s2 =
   let v =
     String.concat " "
@@ -157,16 +160,13 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
         let ids_def = match def with
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Lazyconstr.force cs)
-        | OpaqueDef lc -> 
-            (* we force so that cst are added to the env immediately after *)
-            ignore(Future.join cst);
-            let vars =
-              global_vars_set env (Lazyconstr.force_opaque (Future.join lc)) in
+        | OpaqueDef lc ->
+            let vars = global_vars_set env (Lazyconstr.force_opaque lc) in
             !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;
             vars
-            in
+        in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.compilation_mode = Flags.BuildVo then
@@ -184,12 +184,11 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
-            OpaqueDef (Future.chain ~greedy:true ~pure:true lc (fun lc ->
+            OpaqueDef (Lazyconstr.iter_direct_lazy_constr (fun c ->
               let ids_typ = global_vars_set_constant_type env typ in
-              let ids_def =
-                global_vars_set env (Lazyconstr.force_opaque lc) in
+              let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
-              check declared inferred; lc)) in
+              check declared inferred) lc) in
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
@@ -200,8 +199,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
 (*s Global and local constant declaration. *)
 
 let translate_constant env kn ce =
-  build_constant_declaration kn env 
-    (infer_declaration ~what:(string_of_con kn) env ce)
+  build_constant_declaration kn env (infer_declaration env ce)
 
 let translate_recipe env kn r =
   let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
@@ -209,7 +207,7 @@ let translate_recipe env kn r =
 
 let translate_local_def env id centry =
   let def,typ,cst,inline_code,ctx =
-    infer_declaration ~what:(string_of_id id) env (DefinitionEntry centry) in
+    infer_declaration env (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   def, typ, cst
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 6f71ecd82..b1c336ad9 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,7 +14,7 @@ open Declarations
 open Entries
 
 val translate_local_def : env -> Id.t -> definition_entry ->
-  constant_def * types * constant_constraints
+  constant_def * types * Univ.constraints
 
 val translate_local_assum : env -> types -> types * constraints
 
@@ -32,7 +32,7 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : ?what:string -> env -> constant_entry -> Cooking.result
+val infer_declaration : env -> constant_entry -> Cooking.result
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 9832ba587..91e28132a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,7 +45,7 @@ let boot = ref false
 
 let batch_mode = ref false
 
-type compilation_mode = BuildVo | BuildVi
+type compilation_mode = BuildVo | BuildVi | Vi2Vo
 let compilation_mode = ref BuildVo
 
 type async_proofs = APoff | APonLazy | APonParallel of int
diff --git a/lib/flags.mli b/lib/flags.mli
index ecaa11388..6c6aa5fbe 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -11,7 +11,7 @@
 val boot : bool ref
 
 val batch_mode : bool ref
-type compilation_mode = BuildVo | BuildVi
+type compilation_mode = BuildVo | BuildVi | Vi2Vo
 val compilation_mode : compilation_mode ref
 
 type async_proofs = APoff | APonLazy | APonParallel of int
diff --git a/library/declare.ml b/library/declare.ml
index 3bd4cdd3f..477e96bd8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -117,7 +117,13 @@ let open_constant i ((sp,kn), obj) =
   if obj.cst_locl then ()
   else
     let con = Global.constant_of_delta_kn kn in
-    Nametab.push (Nametab.Exactly i) sp (ConstRef con)
+    Nametab.push (Nametab.Exactly i) sp (ConstRef con);
+    match (Global.lookup_constant con).const_body with
+    | (Def _ | Undef _) -> ()
+    | OpaqueDef lc ->
+        match Lazyconstr.get_opaque_future_constraints lc with
+        | Some f when Future.is_val f -> Global.add_constraints (Future.force f)
+        | _ -> ()
 
 let exists_name id =
   variable_exists id || Global.exists_objlabel (Label.of_id id)
@@ -144,12 +150,12 @@ let discharged_hyps kn sechyps =
 
 let discharge_constant ((sp, kn), obj) =
   let con = constant_of_kn kn in
-  let cb = Global.lookup_constant con in
-  let repl = replacement_context () in
-  let sechyps = section_segment_of_constant con in
-  let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in
-  let new_hyps = (discharged_hyps kn sechyps) @ obj.cst_hyps in
-  let new_decl = GlobalRecipe recipe in
+  let from = Global.lookup_constant con in
+  let modlist = replacement_context () in
+  let hyps = section_segment_of_constant con in
+  let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
+  let abstract = named_of_variable_context hyps in
+  let new_decl = GlobalRecipe{ from; info = { Lazyconstr.modlist; abstract }} in
   Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -192,8 +198,7 @@ let declare_sideff se =
   let pt_opaque_of cb =
     match cb with
     | { const_body = Def sc } -> Lazyconstr.force sc, false
-    | { const_body = OpaqueDef fc } ->
-          Lazyconstr.force_opaque (Future.force fc), true
+    | { const_body = OpaqueDef fc } -> Lazyconstr.force_opaque fc, true
     | { const_body = Undef _ } -> anomaly(str"Undefined side effect")
   in
   let ty_of cb =
diff --git a/library/lib.ml b/library/lib.ml
index eef8171cc..ee89bb997 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -385,7 +385,7 @@ type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap
 
 let sectab =
   Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
-		        Cooking.work_list * abstr_list) list)
+		        Lazyconstr.work_list * abstr_list) list)
     ~name:"section-context"
 
 let add_section () =
@@ -455,6 +455,13 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
+let full_replacement_context () = List.map pi2 !sectab
+let full_section_segment_of_constant con =
+  List.map (fun (vars,_,(x,_)) -> fun hyps ->
+    named_of_variable_context
+      (try Names.Cmap.find con x
+      with Not_found -> extract_hyps (vars, hyps))) !sectab
+
 (*************)
 (* Sections. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index fa3bd3f48..787dc969e 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -186,4 +186,9 @@ val discharge_con : Names.constant -> Names.constant
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
 
+(* discharging a constant in one go *)
+val full_replacement_context : unit -> Lazyconstr.work_list list
+val full_section_segment_of_constant :
+  Names.constant -> (Context.named_context -> Context.named_context) list
+
 
diff --git a/library/library.ml b/library/library.ml
index 1088bcb16..c40f9d204 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -299,12 +299,10 @@ exception Faulty
 (** Fetching a table of opaque terms at position [pos] in file [f],
     expecting to find first a copy of [digest]. *)
 
-let fetch_opaque_table dp (f,pos,digest) =
-  if !Flags.load_proofs == Flags.Dont then
-    error "Not accessing an opaque term due to option -dont-load-proofs.";
+let fetch_table what dp (f,pos,digest) =
   let dir_path = Names.DirPath.to_string dp in
   try
-    Pp.msg_info (Pp.str "Fetching opaque terms from disk for " ++ str dir_path);
+    msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
     let ch = System.with_magic_number_check raw_intern_library f in
     let () = seek_in ch pos in
     if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
@@ -316,64 +314,129 @@ let fetch_opaque_table dp (f,pos,digest) =
     table
   with e when Errors.noncritical e ->
     error
-      ("The file "^f^" (bound to " ^ dir_path ^ ") is inaccessible or corrupted,\n"
-       ^ "cannot load some opaque constant bodies in it.\n")
+      ("The file "^f^" (bound to " ^ dir_path ^
+      ") is inaccessible or corrupted,\n" ^
+      "cannot load some "^what^" in it.\n")
 
 (** Delayed / available tables of opaque terms *)
 
-type opaque_table_status =
+type 'a table_status =
   | ToFetch of string * int * Digest.t
-  | Fetched of Term.constr array
+  | Fetched of 'a Future.computation array
 
-let opaque_tables = ref (LibraryMap.empty : opaque_table_status LibraryMap.t)
+let opaque_tables =
+  ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
+let univ_tables =
+  ref (LibraryMap.empty : (Univ.constraints table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
+let add_univ_table dp st =
+  univ_tables := LibraryMap.add dp st !univ_tables
 
-let access_opaque_table dp i =
-  let t = match LibraryMap.find dp !opaque_tables with
+let access_table fetch_table add_table tables dp i =
+  let t = match LibraryMap.find dp tables with
     | Fetched t -> t
     | ToFetch (f,pos,digest) ->
-      let t = fetch_opaque_table dp (f,pos,digest) in
-      add_opaque_table dp (Fetched t);
+      let t = fetch_table dp (f,pos,digest) in
+      add_table dp (Fetched t);
       t
   in
   assert (i < Array.length t); t.(i)
 
+let access_opaque_table dp i =
+  if !Flags.load_proofs == Flags.Dont then
+    error "Not accessing an opaque term due to option -dont-load-proofs.";
+  access_table
+    (fetch_table "opaque proofs")
+    add_opaque_table !opaque_tables dp i
+let access_univ_table dp i =
+  access_table
+    (fetch_table "universe constraints of opaque proofs")
+    add_univ_table !univ_tables dp i
+
 (** Table of opaque terms from the library currently being compiled *)
 
 module OpaqueTables = struct
 
- let a_constr = Term.mkRel 1
+ let a_constr = Future.from_val (Term.mkRel 1)
+ let a_univ = Future.from_val Univ.empty_constraint
+ let a_discharge : Lazyconstr.cooking_info list = []
 
- let local_table = ref (Array.make 100 a_constr)
+ let local_opaque_table = ref (Array.make 100 a_constr)
+ let local_univ_table = ref (Array.make 100 a_univ)
+ let local_discharge_table = ref (Array.make 100 a_discharge)
  let local_index = ref 0
 
- let get dp i =
+ module FMap = Map.Make(Future.UUID)
+ let f2t = ref FMap.empty
+
+ let get_opaque_nolib _ i = (!local_opaque_table).(i)
+
+ let get_opaque dp i =
    if DirPath.equal dp (Lib.library_dp ())
-   then (!local_table).(i)
+   then (!local_opaque_table).(i)
    else access_opaque_table dp i
+ 
+ let join_local_opaque dp i =
+   if DirPath.equal dp (Lib.library_dp ()) then
+    Future.sink (!local_opaque_table).(i)
 
- let store c =
+ let join_local_univ dp i =
+   if DirPath.equal dp (Lib.library_dp ()) then
+    Future.sink (!local_univ_table).(i)
+
+ let get_univ_nolib _ i = Some (!local_univ_table).(i)
+
+ let get_univ dp i =
+   if DirPath.equal dp (Lib.library_dp ())
+   then Some (!local_univ_table).(i)
+   else try Some (access_univ_table dp i) with Not_found -> None
+
+ let store (d,cu) =
   let n = !local_index in
   incr local_index;
-  if Int.equal n (Array.length !local_table) then begin
+  if Int.equal n (Array.length !local_opaque_table) then begin
     let t = Array.make (2*n) a_constr in
-    Array.blit !local_table 0 t 0 n;
-    local_table := t
+    Array.blit !local_opaque_table 0 t 0 n;
+    local_opaque_table := t;
+    let t = Array.make (2*n) a_univ in
+    Array.blit !local_univ_table 0 t 0 n;
+    local_univ_table := t;
+    let t = Array.make (2*n) a_discharge in
+    Array.blit !local_discharge_table 0 t 0 n;
+    local_discharge_table := t
   end;
-  (!local_table).(n) <- c;
+  let c, u = Future.split2 ~greedy:true cu in
+  if Future.is_val u then ignore(Future.join u);
+  if Future.is_val c then ignore(Future.join c);
+  (!local_opaque_table).(n) <- c;
+  (!local_univ_table).(n) <- u;
+  (!local_discharge_table).(n) <- d;
+  f2t := FMap.add (Future.uuid cu) n !f2t;
   Some (Lib.library_dp (), n)
 
- let dump () = Array.sub !local_table 0 !local_index
+ let dump () =
+   Array.sub !local_opaque_table 0 !local_index,
+   Array.sub !local_univ_table 0 !local_index,
+   Array.sub !local_discharge_table 0 !local_index,
+   FMap.bindings !f2t
 
 end
 
-let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get
+let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque
+let _ = Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ
+let _ = Lazyconstr.set_join_indirect_local_opaque OpaqueTables.join_local_opaque
+let _ = Lazyconstr.set_join_indirect_local_univ OpaqueTables.join_local_univ
 
 (************************************************************************)
 (* Internalise libraries *)
 
+type seg_lib = library_disk
+type seg_univ = Univ.constraints Future.computation array
+type seg_discharge = Lazyconstr.cooking_info list array
+type seg_proofs = Term.constr Future.computation array
+
 let mk_library md digest =
   {
     library_name     = md.md_name;
@@ -386,7 +449,10 @@ let mk_library md digest =
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-  let lmd, _, digest_lmd = System.marshal_in_segment f ch 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 _ = System.skip_in_segment f ch in
   let pos, digest = System.skip_in_segment f ch in
   register_library_filename lmd.md_name f;
   add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
@@ -394,18 +460,6 @@ let intern_from_file f =
   close_in ch;
   library
 
-let load_library_todo f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
-  let f = longf^"i" in
-  let ch = System.with_magic_number_check raw_intern_library f in
-  let _ = System.skip_in_segment f ch in
-  let tasks, _, _ = System.marshal_in_segment f ch in
-  match tasks with
-  | Some a -> a, longf
-  | None -> errorlabstrm "load_library_todo" (str"not a .vi file")
-
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
   try find_library dir, needed
@@ -604,10 +658,27 @@ let start_library f =
   let id = Id.of_string (Filename.basename f) in
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
-  Lazyconstr.set_indirect_opaque_creator OpaqueTables.store;
+  Lazyconstr.set_indirect_creator OpaqueTables.store;
   Declaremods.start_library ldir;
   ldir,longf
 
+let load_library_todo f =
+  let paths = Loadpath.get_paths () in
+  let _, longf =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let f = longf^"i" in
+  let ch = System.with_magic_number_check raw_intern_library f in
+  let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
+  let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
+  let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
+  let tasks, _, _ = System.marshal_in_segment f ch in
+  let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+  close_in ch;
+  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");
+  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. *)
 
@@ -635,10 +706,25 @@ let error_recursively_dependent_library dir =
    writing the content and computing the checksum... *)
 
 let save_library_to ?todo dir f =
-  let f = if todo = None then f ^ "o" else f ^ "i" in
-  Lazyconstr.reset_indirect_opaque_creator ();
+  let f, todo, utab, dtab =
+    match todo with
+    | None ->
+        assert(!Flags.compilation_mode = Flags.BuildVo);
+        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
+  Lazyconstr.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
+   * accessors use Lib.  Hence *)
+  Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib;
+  Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ_nolib;
   let cenv, seg, ast = Declaremods.end_library dir in
-  let table = OpaqueTables.dump () in
+  let opaque_table, univ_table, disch_table, f2t_map =
+    OpaqueTables.dump () in
+  assert(!Flags.compilation_mode = Flags.BuildVi ||
+         Array.for_all Future.is_val opaque_table);
   let md = {
     md_name = dir;
     md_compiled = cenv;
@@ -651,9 +737,11 @@ let save_library_to ?todo dir f =
   let (f',ch) = raw_extern_library f in
   try
     (* Writing vo payload *)
-    System.marshal_out_segment f' ch md;    (* env + objs *)
-    System.marshal_out_segment f' ch todo;  (* STM tasks  *)
-    System.marshal_out_segment f' ch table; (* opaques    *)
+    System.marshal_out_segment f' ch (md               : seg_lib);
+    System.marshal_out_segment f' ch (utab univ_table  : seg_univ option);
+    System.marshal_out_segment f' ch (dtab disch_table : seg_discharge option);
+    System.marshal_out_segment f' ch (todo f2t_map     : 'tasks option);
+    System.marshal_out_segment f' ch (opaque_table     : seg_proofs);
     close_out ch;
     (* Writing native code files *)
     if not !Flags.no_native_compiler then
@@ -662,7 +750,7 @@ let save_library_to ?todo dir f =
       let lp = List.map map_path lp in
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then
-        msg_error (str "Could not compile the library to native code. Skipping.")
+        msg_error (str"Could not compile the library to native code. Skipping.")
    with reraise ->
     let reraise = Errors.push reraise in
     let () = msg_warning (str ("Removed file "^f')) in
@@ -670,6 +758,15 @@ let save_library_to ?todo dir f =
     let () = Sys.remove f' in
     raise reraise
 
+let save_library_raw f lib univs proofs =
+  let (f',ch) = raw_extern_library (f^"o") in
+  System.marshal_out_segment f' ch (lib        : seg_lib);
+  System.marshal_out_segment f' ch (Some univs : seg_univ option);
+  System.marshal_out_segment f' ch (None       : seg_discharge option);
+  System.marshal_out_segment f' ch (None       : 'tasks option);
+  System.marshal_out_segment f' ch (proofs     : seg_proofs);
+  close_out ch
+
 (************************************************************************)
 (*s Display the memory use of a library. *)
 
diff --git a/library/library.mli b/library/library.mli
index 647138483..ec39059e9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -29,6 +29,13 @@ val require_library_from_file :
   Id.t option -> CUnix.physical_path -> bool option -> unit
 
 (** {6 ... } *)
+
+(** Segments of a library *)
+type seg_lib
+type seg_univ = Univ.constraints Future.computation array
+type seg_discharge = Lazyconstr.cooking_info list array
+type seg_proofs = Term.constr Future.computation array
+
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located -> unit
@@ -37,8 +44,12 @@ val import_module : bool -> qualid located -> unit
 val start_library : string -> DirPath.t * string
 
 (** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : ?todo:'a -> DirPath.t -> string -> unit
-val load_library_todo : string -> 'a * string
+val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) ->
+  DirPath.t -> string -> unit
+
+val load_library_todo :
+  string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit
 
 (** {6 Interrogate the status of libraries } *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c6bb9faa0..6fc1973d0 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -999,7 +999,7 @@ let extract_constant env kn cb =
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
-              mk_typ (Lazyconstr.force_opaque (Future.force c))
+              mk_typ (Lazyconstr.force_opaque c)
             else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
@@ -1008,7 +1008,7 @@ let extract_constant env kn cb =
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
-              mk_def (Lazyconstr.force_opaque (Future.force c))
+              mk_def (Lazyconstr.force_opaque c)
             else mk_ax ())
 
 let extract_constant_spec env kn cb =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e8b0295cc..da230ee0d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -385,11 +385,11 @@ let print_constant with_values sep sp =
 	str"*** [ " ++
 	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_univ_cstr (Future.force cb.const_constraints)
+	Printer.pr_univ_cstr (Declareops.constraints_of_constant cb)
     | _ ->
 	print_basename sp ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
-        Printer.pr_univ_cstr (Future.force cb.const_constraints))
+        Printer.pr_univ_cstr (Declareops.constraints_of_constant cb))
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
@@ -531,8 +531,7 @@ let print_full_pure_context () =
 	      | OpaqueDef lc ->
 		str "Theorem " ++ print_basename con ++ cut () ++
 		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
-		str "Proof " ++ pr_lconstr
-                  (Lazyconstr.force_opaque (Future.force lc))
+		str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc)
 	      | Def c ->
 		str "Definition " ++ print_basename con ++ cut () ++
 		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7d225a470..07c91c8d5 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -136,7 +136,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
 let constr_of_def = function
   | Declarations.Undef _ -> assert false
   | Declarations.Def cs -> Lazyconstr.force cs
-  | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc)
+  | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque lc
 
 let build_by_tactic env typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 74a94465e..8a133fc48 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -355,6 +355,7 @@ let parse_args arglist =
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
     |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
+    |"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo
 
     (* Options with zero arg *)
     |"-batch" -> set_batch_mode ()
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index a74f69456..aa64e3f22 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -10,6 +10,7 @@ open Context
 open Cooking
 open Declarations
 open Entries
+open Lazyconstr
 
 val process_inductive :
   named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 9e3d943c0..e73774c97 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -635,9 +635,13 @@ module Slaves : sig
     (?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit
 
   type tasks
-  val dump : unit -> tasks
+  val dump : (Future.UUID.t * int) list -> tasks
   val check_task : string -> tasks -> int -> bool
   val info_tasks : tasks -> (string * float * int) list
+  val finish_task :
+    string ->
+    Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+    tasks -> int -> unit
 
   val cancel_worker : int -> unit
 
@@ -762,11 +766,11 @@ end = struct (* {{{ *)
   let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
   let set_reach_known_state f = reach_known_state := f
 
-  type request =
+  type 'a request =
     ReqBuildProof of
-      (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * string
+      (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * 'a * string
 
-  let name_of_request (ReqBuildProof (_,_,_,_,s)) = s
+  let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
 
   type response =
     | RespBuiltProof of Entries.proof_output list 
@@ -791,19 +795,19 @@ end = struct (* {{{ *)
   type task =
     | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
         (Entries.proof_output list Future.assignement -> unit) * cancel_switch
-        * Loc.t * string
+        * Loc.t * Future.UUID.t * string
   let pr_task = function
-    | TaskBuildProof(_,bop,eop,_,_,_,s) ->
+    | TaskBuildProof(_,bop,eop,_,_,_,_,s) ->
         "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
           ","^s^")"
 
-  let request_of_task task =
+  let request_of_task task : Future.UUID.t request =
     match task with
-    | TaskBuildProof (exn_info,bop,eop,_,_,loc,s) ->
-        ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,s)
+    | TaskBuildProof (exn_info,bop,eop,_,_,loc,uuid,s) ->
+        ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,uuid,s)
 
   let cancel_switch_of_task = function
-    | TaskBuildProof (_,_,_,_,c,_,_) -> c
+    | TaskBuildProof (_,_,_,_,c,_,_,_) -> c
 
   let build_proof_here_core loc eop () =
     let wall_clock1 = Unix.gettimeofday () in
@@ -818,25 +822,24 @@ end = struct (* {{{ *)
 
   let slave_respond msg =
     match msg with
-    | ReqBuildProof(exn_info,eop,vcs,loc,_) ->
+    | ReqBuildProof(exn_info,eop,vcs,loc,_,_) ->
         VCS.restore vcs;
         VCS.print ();
         let r = RespBuiltProof (
           let l = Future.force (build_proof_here exn_info loc eop) in
           List.iter (fun (_,se) -> Declareops.iter_side_effects (function
             | Declarations.SEsubproof(_,
-               { Declarations.const_body = Declarations.OpaqueDef f;
-                 const_constraints = cst} ) -> 
-                  ignore(Future.join f); ignore(Future.join cst)
+               { Declarations.const_body = Declarations.OpaqueDef f } ) ->
+               Lazyconstr.join_lazy_constr f
             | _ -> ())
           se) l;
           l) in
         VCS.print ();
         r
 
-  let check_task name l i =
+  let check_task_aux name l i =
     match List.nth l i with
-    | ReqBuildProof ((id,valid),eop,vcs,loc,s) ->
+    | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) as req ->
         Pp.msg_info(str(Printf.sprintf "Checking task %d (%s) of %s" i s name));
         VCS.restore vcs;
         try
@@ -848,7 +851,7 @@ end = struct (* {{{ *)
           vernac_interp eop ~proof
             { verbose = false; loc;
               expr = (VernacEndProof (Proved (true,None))) };
-          true
+          Some (req,proof)
         with e -> (try
           match Stateid.get e with
           | None ->
@@ -872,10 +875,38 @@ end = struct (* {{{ *)
                     spc () ++ print e)
         with e ->
           Pp.msg_error (str"unable to print error message: " ++
-                        str (Printexc.to_string e))); false
+                        str (Printexc.to_string e))); None
+
+  let finish_task name u d p l i =
+    match check_task_aux name l i with
+    | None -> exit 1
+    | Some (ReqBuildProof ((id,valid),eop,vcs,loc,bucket,s), (po,pt)) ->
+        let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
+        let con =
+          Nametab.locate_constant
+            (Libnames.qualid_of_ident po.Proof_global.id) in
+        let c = Global.lookup_constant con in
+        match c.Declarations.const_body with
+        | Declarations.OpaqueDef lc ->
+            let pr, uc = Lazyconstr.get_opaque_futures lc in
+            let pr = Future.chain ~greedy:true ~pure:true pr discharge in
+            let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+            ignore(Future.join pr);
+            ignore(Future.join uc);
+            Pp.msg_info(str(Printf.sprintf
+              "Assigning output of task %d (%s) of %s to bucket %d"
+              i s name bucket));
+            u.(bucket) <- uc;
+            p.(bucket) <- pr
+        | _ -> assert false
+  
+  let check_task name l i =
+    match check_task_aux name l i with
+    | Some _ -> true
+    | None -> false
 
   let info_tasks l =
-    CList.map_i (fun i (ReqBuildProof(_,_,_,loc,s)) ->
+    CList.map_i (fun i (ReqBuildProof(_,_,_,loc,_,s)) ->
       let time1 =
         try float_of_string (Aux_file.get !hints loc "proof_build_time")
         with Not_found -> 0.0 in
@@ -894,13 +925,13 @@ end = struct (* {{{ *)
 
   let marshal_err s = raise (MarshalError s)
 
-  let marshal_request oc (req : request) =
+  let marshal_request oc (req : Future.UUID.t request) =
     try marshal_to_channel oc req
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("marshal_request: "^s)
 
   let unmarshal_request ic =
-    try (Marshal.from_channel ic : request)
+    try (Marshal.from_channel ic : Future.UUID.t request)
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("unmarshal_request: "^s)
 
@@ -938,16 +969,18 @@ end = struct (* {{{ *)
         let force () : Entries.proof_output list Future.assignement =
           try `Val (build_proof_here_core loc stop ()) with e -> `Exn e in
         let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
+        let uuid = Future.uuid f in
         TQueue.push queue
-          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
+          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
         f, cancel_switch
       end else
         build_proof_here exn_info loc stop, cancel_switch
     else 
       let f, assign = Future.create_delegate (State.exn_on id ~valid) in
+      let uuid = Future.uuid f in
       Pp.feedback (Interface.InProgress 1);
       TQueue.push queue
-        (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
+        (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
       f, cancel_switch
 
   exception RemoteException of std_ppcmds
@@ -991,13 +1024,13 @@ end = struct (* {{{ *)
           let rec loop () =
             let response = unmarshal_response ic in
             match task, response with
-            | TaskBuildProof(_,_,_, assign,_,_,_), RespBuiltProof pl ->
+            | TaskBuildProof(_,_,_, assign,_,_,_,_), RespBuiltProof pl ->
                 assign (`Val pl);
                 (* We restart the slave, to avoid memory leaks.  We could just
                    Pp.feedback (Interface.InProgress ~-1) *)
                 last_task := None;
                 raise KillRespawn
-            | TaskBuildProof(_,_,_, assign,_,_,_),RespError(err_id,valid,e,s) ->
+            | TaskBuildProof(_,_,_, assign,_,_,_,_),RespError(err_id,valid,e,s) ->
                 let e = Stateid.add ~valid (RemoteException e) err_id in
                 assign (`Exn e);
                 Option.iter (State.assign valid) s;
@@ -1029,7 +1062,7 @@ end = struct (* {{{ *)
             msg_warning(strbrk("Marshalling error: "^s^". "^
               "The system state could not be sent to the worker process. "^
               "Falling back to local, lazy, evaluation."));
-            let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+            let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
             assign(`Comp(build_proof_here exn_info loc stop));
             Pp.feedback (Interface.InProgress ~-1)
         | MarshalError s ->
@@ -1052,7 +1085,7 @@ end = struct (* {{{ *)
     | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled ->
         msg_warning(strbrk "The worker was cancelled.");
         Option.iter (fun task ->
-          let TaskBuildProof (_, start, _, assign, _,_,_) = task in
+          let TaskBuildProof (_, start, _, assign, _,_,_,_) = task in
           let s = "Worker cancelled by the user" in
           let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in
           assign (`Exn e);
@@ -1066,7 +1099,7 @@ end = struct (* {{{ *)
         msg_warning(strbrk "The worker process died badly.");
         Option.iter (fun task ->
           msg_warning(strbrk "Falling back to local, lazy, evaluation.");
-          let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+          let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
           assign(`Comp(build_proof_here exn_info loc stop));
           Pp.feedback (Interface.InProgress ~-1);
         ) !last_task;
@@ -1158,13 +1191,14 @@ end = struct (* {{{ *)
     done
 
   (* For external users this name is nicer than request *)
-  type tasks = request list
-  let dump () =
+  type tasks = int request list
+  let dump f2t_map =
     assert(SlavesPool.is_empty ()); (* ATM, we allow that only if no slaves *)
     let tasks = TQueue.dump queue in
     prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks));
     let tasks = List.map request_of_task tasks in
-    tasks
+    List.map (function ReqBuildProof(a,b,c,d,x,e) ->
+      ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks
 
 end (* }}} *)
 
@@ -1562,7 +1596,7 @@ let join () =
   VCS.print ()
 
 type tasks = Slaves.tasks
-let dump () = Slaves.dump ()
+let dump x = Slaves.dump x
 let check_task name tasks i =
   let vcs = VCS.backup () in
   try
@@ -1572,6 +1606,16 @@ let check_task name tasks i =
     rc
   with e when Errors.noncritical e -> VCS.restore vcs; false
 let info_tasks tasks = Slaves.info_tasks tasks
+let finish_tasks name u d p tasks =
+  let finish_task (_,_,i) =
+    let vcs = VCS.backup () in
+    Future.purify (Slaves.finish_task name u d p tasks) i;
+    Pp.pperr_flush ();
+    VCS.restore vcs in
+  try List.iter finish_task (info_tasks tasks)
+  with e ->
+    Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e);
+    exit 1
 
 let merge_proof_branch qast keep brname =
   let brinfo = VCS.get_branch brname in
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 0a7473792..c47bacf65 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -44,10 +44,13 @@ val stop_worker : int -> unit
 val join : unit -> unit
 (* To save to disk an incomplete document *)
 type tasks
-val dump : unit -> tasks
+val dump : (Future.UUID.t * int) list -> tasks
 
 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
 
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 6f39725ff..16cc51086 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,10 +18,10 @@ Vernacentries
 Vernac_classifier
 Stm
 Whelp
+Vi_checking
 Vernac
 Ide_slave
 Usage
 Coqloop
 Coqinit
-Vi_checking
 Coqtop
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index abf58df45..b35929fef 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -367,6 +367,14 @@ let compile verbosely f =
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
-      let todo = Stm.dump () in
-      Library.save_library_to ~todo ldir long_f_dot_v
+      Library.save_library_to ~todo:Stm.dump ldir long_f_dot_v
+  | Vi2Vo ->
+      let open Filename in
+      let open Library in
+      Dumpglob.noglob ();
+      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;
+      Library.save_library_raw lfdv lib univs proofs
 
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index a52a83dfe..5fae1c459 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -10,7 +10,7 @@ open Util
 
 let check_vi (ts,f) =
   Dumpglob.noglob ();
-  let tasks, long_f_dot_v = Library.load_library_todo f in
+  let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
   Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
   List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
 
@@ -38,7 +38,7 @@ let schedule_vi_checking j fs =
     let f =
       if Filename.check_suffix f ".vi" then Filename.chop_extension f
       else f in
-    let tasks, long_f_dot_v = Library.load_library_todo f in
+    let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
     Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in