Rework handling of universes on top of the STM, allowing for delayed

computation in case of non-polymorphic proofs. Also fix plugins after
forgotten merge conflicts. Still does not compile everything.

2 files changed, 37 insertions, 16 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7434979f8f..f7548b6ca9 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,7 +68,6 @@ type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  opt_subst : Universes.universe_opt_subst;
 }
 
 type proof_ending =
@@ -268,17 +267,29 @@ let get_open_goals () =
 
 let close_proof ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
+  let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
-  let evdref = ref (Proof.return proof) in
-  let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
-  let initial_goals = List.map (fun (c,t) -> (nf c, nf t)) initial_goals in
-  let ctx = Evd.universe_context !evdref in
+  let fpl, univs = Future.split2 fpl in
+  let () = if poly || now then ignore (Future.compute univs) in
   let entries = Future.map2 (fun p (c, t) ->
-    let univs = 
-      Univ.LSet.union (Universes.universes_of_constr c)
-	(Universes.universes_of_constr t)
-    in 
-    let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) univs in
+    let compute_univs (usubst, uctx) = 
+      let nf = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst in
+      let compute_c_t (c, eff) =
+        let univs =
+          Univ.LSet.union (Universes.universes_of_constr c)
+            (Universes.universes_of_constr t)
+        in 
+        let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context uctx) univs in
+          (nf c, eff), nf t, Univ.ContextSet.to_context ctx
+      in
+        Future.chain ~pure:true p compute_c_t
+    in
+    let ans = Future.chain ~pure:true univs compute_univs in
+    let ans = Future.join ans in
+    let p = Future.chain ~pure:true ans (fun (x, _, _) -> x) in
+    let t = Future.chain ~pure:true ans (fun (_, x, _) -> x) in
+    let univs = Future.chain ~pure:true ans (fun (_, _, x) -> x) in
+    let t = Future.force t in
     { Entries.
     const_entry_body = p;
     const_entry_secctx = section_vars;
@@ -286,14 +297,17 @@ let close_proof ?feedback_id ~now fpl =
     const_entry_feedback = feedback_id;
     const_entry_inline_code = false;
     const_entry_opaque = true;
-    const_entry_universes = Univ.ContextSet.to_context ctx;
+    const_entry_universes = univs;
     const_entry_polymorphic = pi2 strength;
     const_entry_proj = None}) fpl initial_goals in
   if now then
     List.iter (fun x -> ignore(Future.force x.Entries.const_entry_body)) entries;
-  { id = pid; entries = entries; persistence = strength; opt_subst = subst },
+  { id = pid; entries = entries; persistence = strength },
   Ephemeron.get terminator
 
+type closed_proof_output = Entries.proof_output list * 
+    Universes.universe_opt_subst Univ.in_universe_context
+
 let return_proof () =
   let { proof } = cur_pstate () in
   let initial_goals = Proof.initial_goals proof in
@@ -310,10 +324,14 @@ let return_proof () =
         error(str"Attempt to save a proof with existential " ++
               str"variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
+  let evd = Evd.nf_constraints evd in
+  let subst = Evd.universe_subst evd in
+  let ctx = Evd.universe_context evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-  List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals
+  let goals = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals in
+    goals, (subst, ctx)
 
 let close_future_proof ~feedback_id proof =
   close_proof ~feedback_id ~now:false proof
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e651bdfae3..f10e991eab 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -61,7 +61,6 @@ type proof_object = {
   id : Names.Id.t;
   entries : Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  opt_subst : Universes.universe_opt_subst;
 }
 
 type proof_ending =
@@ -95,9 +94,13 @@ val close_proof : (exn -> exn) -> closed_proof
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
  * chained with a computation that completed the proof *)
-val return_proof : unit -> Entries.proof_output list
+
+type closed_proof_output = Entries.proof_output list * 
+    Universes.universe_opt_subst Univ.in_universe_context
+
+val return_proof : unit -> closed_proof_output
 val close_future_proof : feedback_id:Stateid.t ->
-  Entries.proof_output list Future.computation -> closed_proof
+  closed_proof_output Future.computation -> closed_proof
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)