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.

3 files changed, 12 insertions, 17 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 2aeb8141e8..13194eb891 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -229,17 +229,8 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp
         | _ -> anomaly (Pp.str "Not a proof by induction") in
       match locality with
       | Discharge ->
-          let const = { const_entry_body =
-                Future.from_val (body_i,Declareops.no_seff);
-              const_entry_secctx = None;
-              const_entry_type = Some t_i;
-	      const_entry_proj = None;
-              const_entry_opaque = opaq;
-              const_entry_feedback = None;
-              const_entry_inline_code = false;
-	      const_entry_polymorphic = p;
-	      const_entry_universes = Univ.ContextSet.to_context ctx_i
-          } in
+          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
+	    ~univs:(Univ.ContextSet.to_context ctx_i) body_i in
 	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
           (Discharge,VarRef id,imps)
diff --git a/stm/stm.ml b/stm/stm.ml
index 0218c923bf..3496a3e4fc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -70,7 +70,7 @@ let vernac_parse eid s =
   ()
 
 module Vcs_ = Vcs.Make(Stateid)
-type future_proof = Entries.proof_output list Future.computation
+type future_proof = Proof_global.closed_proof_output Future.computation
 type proof_mode = string
 type depth = int
 type cancel_switch = bool ref
@@ -683,7 +683,7 @@ end = struct
   let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
 
   type response =
-    | RespBuiltProof of Entries.proof_output list * float
+    | RespBuiltProof of Proof_global.closed_proof_output * float
     | RespError of (* err, safe, msg, safe_states *)
         Stateid.t * Stateid.t * std_ppcmds *
           (Stateid.t * State.frozen_state) list
@@ -705,8 +705,9 @@ end = struct
  
   type task =
     | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
-        (Entries.proof_output list Future.assignement -> unit) * cancel_switch
+        (Proof_global.closed_proof_output Future.assignement -> unit) * cancel_switch
         * Loc.t * Future.UUID.t * string
+
   let pr_task = function
     | TaskBuildProof(_,bop,eop,_,_,_,_,s) ->
         "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
@@ -745,7 +746,7 @@ end = struct
 		 const_universes = univs } ) ->
                 Opaqueproof.join_opaque f; ignore (Future.join univs) (* FIXME: MS: needed?*)
             | _ -> ())
-          se) l;
+          se) (fst l);
           l, Unix.gettimeofday () -. wall_clock in
         VCS.print ();
         RespBuiltProof(rc,time)
@@ -895,7 +896,7 @@ end = struct
     let cancel_switch = ref false in
     if WorkersPool.is_empty () then
       if !Flags.compilation_mode = Flags.BuildVi then begin
-        let force () : Entries.proof_output list Future.assignement =
+        let force () : Proof_global.closed_proof_output Future.assignement =
           try `Val (build_proof_here_core loc stop ())
           with e -> let e = Errors.push e in `Exn e in
         let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 3bd83f46bc..94268e020e 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -66,7 +66,10 @@ let rec classify_vernac e =
     (* Nested vernac exprs *)
     | VernacProgram e -> classify_vernac e
     | VernacLocal (_,e) -> classify_vernac e
-    | VernacPolymorphic (b, e) -> classify_vernac e
+    | VernacPolymorphic (b, e) -> 
+      if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
+	fst (classify_vernac e), VtNow
+      else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
     | VernacTime e -> classify_vernac e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)