Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

11 files changed, 361 insertions, 194 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 672527d9..e3fb0b60 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -177,7 +177,7 @@ module Make(T : Task) = struct
       if not (Worker.is_alive proc) then ()
       else if cancelled () || !(!expiration_date) then
         let () = stop_waiting := true in
-        let () = TQueue.signal_destruction queue in
+        let () = TQueue.broadcast queue in
         Worker.kill proc
       else
         let () = Unix.sleep 1 in
@@ -253,6 +253,8 @@ module Make(T : Task) = struct
     Pool.destroy active;
     TQueue.destroy queue
 
+  let broadcast { queue } = TQueue.broadcast queue
+
   let enqueue_task { queue; active } (t, _ as item) =
     prerr_endline ("Enqueue task "^T.name_of_task t);
     TQueue.push queue item
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index 78f295d3..a3fe4b8c 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -61,6 +61,8 @@ module MakeQueue(T : Task) : sig
 
   val set_order : queue -> (T.task -> T.task -> int) -> unit
 
+  val broadcast : queue -> unit
+
   (* Take a snapshot (non destructive but waits until all workers are
    * enqueued) *)
   val snapshot : queue -> T.task list
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f2e68779..6cece32e 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -185,7 +185,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -200,7 +200,8 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
           | Local | Discharge -> true
           | Global -> false
           in
-          let kn = declare_constant id ~local (DefinitionEntry const, k) in
+          let kn =
+           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           (locality, ConstRef kn) in
     definition_message id;
     call_hook (fun exn -> exn) hook l r
@@ -273,35 +274,29 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
 let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
-let save_named proof =
+let save_named ?export_seff proof =
   let id,const,cstrs,do_guard,persistence,hook = proof in
-  save id const cstrs do_guard persistence hook
+  save ?export_seff id const cstrs do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
 
-let save_anonymous proof save_ident =
+let save_anonymous ?export_seff proof save_ident =
   let id,const,cstrs,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save save_ident const cstrs do_guard persistence hook
+  save ?export_seff save_ident const cstrs do_guard persistence hook
 
-let save_anonymous_with_strength proof kind save_ident =
+let save_anonymous_with_strength ?export_seff proof kind save_ident =
   let id,const,cstrs,do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+  save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
 
 (* Admitted *)
 
-let admit hook () =
-  let (id,k,typ) = Pfedit.current_proof_statement () in
-  let ctx =
-    let evd = fst (Pfedit.get_current_goal_context ()) in
-      Evd.universe_context evd
-  in
-  let e = Pfedit.get_used_variables(), pi2 k, (typ, ctx), None in
+let admit (id,k,e) hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
@@ -325,34 +320,50 @@ let get_proof proof do_guard hook opacity =
   (** FIXME *)
   id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
 
+let check_exist =
+  List.iter (fun (loc,id) ->
+    if not (Nametab.exists_cci (Lib.make_path id)) then
+        user_err_loc (loc,"",pr_id id ++ str " does not exist.")
+  )
+
 let standard_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted ->
-      admit hook ();
+  | Admitted (id,k,pe) ->
+      admit (id,k,pe) hook ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard hook is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted ->
-      admit (hook None) ();
+  | Admitted (id,k,pe) ->
+      admit (id,k,pe) (hook None) ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard 
 	(hook (Some proof.Proof_global.universes)) is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
@@ -458,7 +469,37 @@ let start_proof_com kind thms hook =
 
 let save_proof ?proof = function
   | Vernacexpr.Admitted ->
-      Proof_global.get_terminator() Proof_global.Admitted
+      let pe =
+        let open Proof_global in
+        match proof with
+        | Some ({ id; entries; persistence = k; universes }, _) ->
+            if List.length entries <> 1 then
+              error "Admitted does not support multiple statements";
+            let { const_entry_secctx; const_entry_type } = List.hd entries in
+            if const_entry_type = None then
+              error "Admitted requires an explicit statement";
+            let typ = Option.get const_entry_type in
+            let ctx = Evd.evar_context_universe_context universes in
+            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None))
+        | None ->
+            let id, k, typ = Pfedit.current_proof_statement () in
+            let ctx =
+              let evd, _ = Pfedit.get_current_goal_context () in
+              Evd.universe_context evd in
+            (* This will warn if the proof is complete *)
+            let pproofs,_ = Proof_global.return_proof ~allow_partial:true () in
+            let sec_vars =
+              match  Pfedit.get_used_variables(), pproofs with
+              | Some _ as x, _ -> x
+              | None, (pproof, _) :: _ -> 
+                  let env = Global.env () in
+                  let ids_typ = Environ.global_vars_set env typ in
+                  let ids_def = Environ.global_vars_set env pproof in
+                  Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
+              | _ -> None in
+            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None))
+      in
+      Proof_global.get_terminator() pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
       let (proof_obj,terminator) =
         match proof with
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index d0669d7a..a0ddd265 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -10,7 +10,6 @@ open Names
 open Term
 open Decl_kinds
 open Constrexpr
-open Tacexpr
 open Vernacexpr
 open Pfedit
 
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 18159288..a8372195 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -81,6 +81,7 @@ let init_channels () =
 
 let get_channels () =
   match !channels with
-  | None -> Errors.anomaly(Pp.str "init_channels not called")
+  | None ->
+    Printf.eprintf "Fatal error: ideslave communication channels not set.\n";
+    exit 1
   | Some(ic, oc) -> ic, oc
-
diff --git a/stm/stm.ml b/stm/stm.ml
index 7b246854..38745e22 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -8,7 +8,8 @@
 
 let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
 
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if false then begin pr_err s end else ()
+let prerr_debug s = if !Flags.debug then begin pr_err s end else ()
 
 open Vernacexpr
 open Errors
@@ -130,8 +131,9 @@ type cancel_switch = bool ref
 type branch_type =
   [ `Master
   | `Proof of proof_mode * depth
-  | `Edit of proof_mode * Stateid.t * Stateid.t ]
+  | `Edit of proof_mode * Stateid.t * Stateid.t  * vernac_qed_type ]
 type cmd_t = {
+  ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
   cast : ast;
   cids : Id.t list;
   cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
@@ -144,7 +146,7 @@ type qed_t = {
   brinfo : branch_type Vcs_.branch_info
 }
 type seff_t = ast option
-type alias_t = Stateid.t
+type alias_t = Stateid.t * ast
 type transaction =
   | Cmd    of cmd_t
   | Fork   of fork_t
@@ -160,6 +162,11 @@ type step =
   | `Alias  of alias_t ]
 type visit = { step : step; next : Stateid.t }
 
+
+(* Parts of the system state that are morally part of the proof state *)
+let summary_pstate = [ Evarutil.meta_counter_summary_name;
+                       Evarutil.evar_counter_summary_name;
+                       "program-tcc-table" ]
 type state = {
   system : States.state;
   proof : Proof_global.state;
@@ -315,7 +322,7 @@ end = struct (* {{{ *)
             (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff None -> "EnvChange"
       | Noop -> " "
-      | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id)
+      | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
       | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
     let is_green id = 
       match get_info vcs id with
@@ -442,7 +449,7 @@ end = struct (* {{{ *)
     if List.mem edit_branch (Vcs_.branches !vcs) then begin
       checkout edit_branch;
       match get_branch edit_branch with
-      | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+      | { kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode
       | _ -> assert false
     end else
       let pl = proof_nesting () in
@@ -593,9 +600,12 @@ module State : sig
   type frozen_state
   val get_cached : Stateid.t -> frozen_state
   val same_env : frozen_state -> frozen_state -> bool
+
+  type proof_part
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  val proof_part_of_frozen : frozen_state -> Proof_global.state
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  val proof_part_of_frozen : frozen_state -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
 end = struct (* {{{ *)
@@ -619,9 +629,14 @@ end = struct (* {{{ *)
     (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
   
   type frozen_state = state
+  type proof_part =
+    Proof_global.state * Summary.frozen_bits (* only meta counters *)
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  let proof_part_of_frozen { proof } = proof
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  let proof_part_of_frozen { proof; system } =
+    proof,
+    Summary.project_summary (States.summary_of_state system) summary_pstate
 
   let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
 
@@ -656,9 +671,16 @@ end = struct (* {{{ *)
     if VCS.get_state id <> None then () else
     try match what with
     | `Full s -> VCS.set_state id s
-    | `Proof(ontop,p) ->
-         if is_cached ontop then (
-           VCS.set_state id { (get_cached ontop) with proof = p })
+    | `Proof(ontop,(pstate,counters)) ->
+         if is_cached ontop then
+           let s = get_cached ontop in
+           let s = { s with proof = pstate } in
+           let s = { s with system =
+             States.replace_summary s.system
+               (Summary.surgery_summary
+                 (States.summary_of_state s.system)
+               counters) } in
+           VCS.set_state id s
     with VCS.Expired -> ()
 
   let exn_on id ?valid (e, info) =
@@ -769,19 +791,20 @@ end = struct (* {{{ *)
     match info.vcs_backup with
     | None, _ -> next acc
     | Some vcs, _ ->
-        let ids =
-          if id = Stateid.initial || id = Stateid.dummy then [] else
+        let ids, tactic, undo =
+          if id = Stateid.initial || id = Stateid.dummy then [],false,0 else
           match VCS.visit id with
-          | { step = `Fork ((_,_,_,l),_) } -> l
-          | { step = `Cmd { cids = l } } -> l
-          | _ -> [] in
-        match f acc (id, vcs, ids) with
+          | { step = `Fork ((_,_,_,l),_) } -> l, false,0
+          | { step = `Cmd { cids = l; ctac } } -> l, ctac,0
+          | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n
+          | _ -> [],false,0 in
+        match f acc (id, vcs, ids, tactic, undo) with
         | `Stop x -> x
         | `Cont acc -> next acc
  
   let back_safe () =
     let id =
-      fold_until (fun n (id,_,_) ->
+      fold_until (fun n (id,_,_,_,_) ->
         if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
         0 (VCS.get_branch_pos (VCS.current_branch ())) in
     backto id
@@ -797,7 +820,7 @@ end = struct (* {{{ *)
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
             let oid =
-              fold_until (fun b (id,_,label) ->
+              fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
             VtStm (VtBack oid, true), VtNow
@@ -805,17 +828,15 @@ end = struct (* {{{ *)
             VtStm (VtBack id, true), VtNow)
       | VernacBack n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_) ->
+          let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
           VtStm (VtBack oid, true), VtNow
       | VernacUndo n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_) ->
-            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode &&
-             not !Flags.print_emacs then
-           VtStm (VtBack oid, false), VtNow
-          else VtStm (VtBack oid, true), VtLater
+          let oid = fold_until (fun n (id,_,_,tactic,undo) ->
+            let value = (if tactic then 1 else 0) - undo in
+            if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
+          VtStm (VtBack oid, true), VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -826,15 +847,15 @@ end = struct (* {{{ *)
             | Some vcs, _ -> vcs in
           let cb, _ =
             Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
-          let n = fold_until (fun n (_,vcs,_) ->
+          let n = fold_until (fun n (_,vcs,_,_,_) ->
             if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
             0 id in
-          let oid = fold_until (fun n (id,_,_) ->
+          let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
           VtStm (VtBack oid, true), VtLater
       | VernacAbortAll ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun () (id,vcs,_) ->
+          let oid = fold_until (fun () (id,vcs,_,_,_) ->
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
           VtStm (VtBack oid, true), VtLater
@@ -885,6 +906,7 @@ module rec ProofTask : sig
     t_exn_info : Stateid.t * Stateid.t;
     t_start    : Stateid.t;
     t_stop     : Stateid.t;
+    t_drop     : bool;
     t_states   : competence;
     t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
     t_loc      : Loc.t;
@@ -896,8 +918,8 @@ module rec ProofTask : sig
     | States of Stateid.t list
 
   type request =
-    | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence
-    | ReqStates of Stateid.t list
+  | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence
+  | ReqStates of Stateid.t list
 
   include AsyncTaskQueue.Task
   with type task := task
@@ -905,9 +927,13 @@ module rec ProofTask : sig
   and  type request := request
 
   val build_proof_here :
+    drop_pt:bool ->
     Stateid.t * Stateid.t -> Loc.t -> Stateid.t ->
       Proof_global.closed_proof_output Future.computation
-   
+
+  (* If set, only tasks overlapping with this list are processed *)
+  val set_perspective : Stateid.t list -> unit  
+
 end = struct (* {{{ *)
 
   let forward_feedback msg = Hooks.(call forward_feedback msg)
@@ -917,6 +943,7 @@ end = struct (* {{{ *)
     t_exn_info : Stateid.t * Stateid.t;
     t_start    : Stateid.t;
     t_stop     : Stateid.t;
+    t_drop     : bool;
     t_states   : competence;
     t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
     t_loc      : Loc.t;
@@ -928,8 +955,8 @@ end = struct (* {{{ *)
     | States of Stateid.t list
 
   type request =
-    | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence
-    | ReqStates of Stateid.t list
+  | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence
+  | ReqStates of Stateid.t list
   
   type error = {
     e_error_at    : Stateid.t;
@@ -946,9 +973,14 @@ end = struct (* {{{ *)
   let name = ref "proofworker"
   let extra_env () = !async_proofs_workers_extra_env
 
+  let perspective = ref []
+  let set_perspective l = perspective := l
+
   let task_match age t =
     match age, t with
-    | `Fresh, BuildProof _ -> true
+    | `Fresh, BuildProof { t_states } ->
+        not !Flags.async_proofs_full ||
+        List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states
     | `Old my_states, States l ->
         List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l
     | _ -> false
@@ -957,12 +989,14 @@ end = struct (* {{{ *)
     | BuildProof t -> "proof: " ^ t.t_name
     | States l -> "states: " ^ String.concat "," (List.map Stateid.to_string l)
   let name_of_request = function
-    | ReqBuildProof(r,_) -> "proof: " ^ r.Stateid.name
+    | ReqBuildProof(r,_,_) -> "proof: " ^ r.Stateid.name
     | ReqStates l -> "states: "^String.concat "," (List.map Stateid.to_string l)
 
   let request_of_task age = function
     | States l -> Some (ReqStates l)
-    | BuildProof { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states } ->
+    | BuildProof {
+        t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states;t_drop
+      } ->
         assert(age = `Fresh);
         try Some (ReqBuildProof ({
           Stateid.exn_info = t_exn_info;
@@ -970,20 +1004,21 @@ end = struct (* {{{ *)
           document = VCS.slice ~start:t_start ~stop:t_stop;
           loc = t_loc;
           uuid = t_uuid;
-          name = t_name }, t_states))
+          name = t_name }, t_drop, t_states))
         with VCS.Expired -> None
 
   let use_response (s : competence AsyncTaskQueue.worker_status) t r =
     match s, t, r with
     | `Old c, States _, RespStates l ->
         List.iter (fun (id,s) -> State.assign id s) l; `End
-    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
+    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
               RespBuiltProof (pl, time) ->
         feedback (Feedback.InProgress ~-1);
         t_assign (`Val pl);
         record_pb_time t_name t_loc time;
-        if not !Flags.async_proofs_full then `End
-        else `Stay(t_states,[States t_states])
+        if !Flags.async_proofs_full || t_drop
+        then `Stay(t_states,[States t_states])
+        else `End
     | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
             RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
         feedback (Feedback.InProgress ~-1);
@@ -1004,7 +1039,7 @@ end = struct (* {{{ *)
         Hooks.(call execution_error start Loc.ghost (strbrk s));
         feedback (Feedback.InProgress ~-1)
 
-  let build_proof_here (id,valid) loc eop =
+  let build_proof_here ~drop_pt (id,valid) loc eop =
     Future.create (State.exn_on id ~valid) (fun () ->
       let wall_clock1 = Unix.gettimeofday () in
       if !Flags.batch_mode then Reach.known_state ~cache:`No eop
@@ -1012,34 +1047,38 @@ end = struct (* {{{ *)
       let wall_clock2 = Unix.gettimeofday () in
       Aux_file.record_in_aux_at loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
-      Proof_global.return_proof ())
+      let p = Proof_global.return_proof ~allow_partial:drop_pt () in
+      if drop_pt then Pp.feedback ~state_id:id Feedback.Complete;
+      p)
 
-  let perform_buildp { Stateid.exn_info; stop; document; loc } my_states =
+  let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
     try
       VCS.restore document;
       VCS.print ();
       let proof, future_proof, time =
         let wall_clock = Unix.gettimeofday () in
-        let fp = build_proof_here exn_info loc stop in
+        let fp = build_proof_here ~drop_pt:drop exn_info loc stop in
         let proof = Future.force fp in
         proof, fp, Unix.gettimeofday () -. wall_clock in
       (* We typecheck the proof with the kernel (in the worker) to spot
        * the few errors tactics don't catch, like the "fix" tactic building
        * a bad fixpoint *)
       let fix_exn = Future.fix_exn_of future_proof in
-      let checked_proof = Future.chain ~pure:false future_proof (fun p ->
-        let pobject, _ =
-          Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
-        let terminator = (* The one sent by master is an InvalidKey *)
-          Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
-        vernac_interp stop
-          ~proof:(pobject, terminator)
-          { verbose = false; loc;
-            expr = (VernacEndProof (Proved (true,None))) }) in
-      ignore(Future.join checked_proof);
+      if not drop then begin
+        let checked_proof = Future.chain ~pure:false future_proof (fun p ->
+          let pobject, _ =
+            Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
+          let terminator = (* The one sent by master is an InvalidKey *)
+            Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
+          vernac_interp stop
+            ~proof:(pobject, terminator)
+            { verbose = false; loc;
+              expr = (VernacEndProof (Proved (Opaque None,None))) }) in
+        ignore(Future.join checked_proof);
+      end;
       RespBuiltProof(proof,time)
     with
-    | e when Errors.noncritical e ->
+    | e when Errors.noncritical e || e = Stack_overflow ->
         let (e, info) = Errors.push e in
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)
@@ -1054,6 +1093,9 @@ end = struct (* {{{ *)
   
   let perform_states query =
     if query = [] then [] else
+    let is_tac = function
+      | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
+      | _ -> false in
     let initial = 
       let rec aux id =
         try match VCS.visit id with { next } -> aux next
@@ -1071,8 +1113,8 @@ end = struct (* {{{ *)
         if State.is_cached id then Some (State.get_cached id) else None in
       match prev, this with
       | _, None -> None
-      | Some (prev, o, `Cmd { cast = { expr = VernacSolve _ }}), Some n
-        when State.same_env o n -> (* A pure tactic *)
+      | Some (prev, o, `Cmd { cast = { expr }}), Some n
+        when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
           msg_warning (str "Sending back a fat state");
@@ -1087,17 +1129,17 @@ end = struct (* {{{ *)
     aux [initial] query
 
   let perform = function
-    | ReqBuildProof (bp,states) -> perform_buildp bp states
+    | ReqBuildProof (bp,drop,states) -> perform_buildp bp drop states
     | ReqStates sl -> RespStates (perform_states sl)
 
   let on_marshal_error s = function
     | States _ -> msg_error(strbrk("Marshalling error: "^s^". "^
         "The system state could not be sent to the master process."))
-    | BuildProof { t_exn_info; t_stop; t_assign; t_loc } ->
+    | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } ->
       msg_error(strbrk("Marshalling error: "^s^". "^
         "The system state could not be sent to the worker process. "^
         "Falling back to local, lazy, evaluation."));
-      t_assign(`Comp(build_proof_here t_exn_info t_loc t_stop));
+      t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop));
       feedback (Feedback.InProgress ~-1)
 
 end (* }}} *)
@@ -1106,7 +1148,8 @@ end (* }}} *)
 and Slaves : sig
 
   (* (eventually) remote calls *)
-  val build_proof : loc:Loc.t ->
+  val build_proof :
+    loc:Loc.t -> drop_pt:bool ->
     exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t ->
       name:string -> future_proof * cancel_switch
 
@@ -1116,7 +1159,7 @@ and Slaves : sig
   (* initialize the whole machinery (optional) *)
   val init : unit -> unit
 
-  type 'a tasks = ('a,VCS.vcs) Stateid.request list
+  type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list
   val dump_snapshot : unit -> Future.UUID.t tasks
   val check_task : string -> int tasks -> int -> bool
   val info_tasks : 'a tasks -> (string * float * int) list
@@ -1144,7 +1187,7 @@ end = struct (* {{{ *)
       queue := Some (TaskQueue.create 0)
 
   let check_task_aux extra name l i =
-    let { Stateid.stop; document; loc; name = r_name } = List.nth l i in
+    let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
     msg_info(
       str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
     VCS.restore document;
@@ -1155,6 +1198,10 @@ end = struct (* {{{ *)
       aux stop in
     try
       Reach.known_state ~cache:`No stop;
+      if drop then
+        let _proof = Proof_global.return_proof ~allow_partial:true () in
+        `OK_ADMITTED
+      else begin
       (* The original terminator, a hook, has not been saved in the .vio*)
       Proof_global.set_terminator
         (Lemmas.standard_proof_terminator []
@@ -1166,8 +1213,9 @@ end = struct (* {{{ *)
       Reach.known_state ~cache:`No start;
       vernac_interp stop ~proof
         { verbose = false; loc;
-          expr = (VernacEndProof (Proved (true,None))) };
-      Some proof
+          expr = (VernacEndProof (Proved (Opaque None,None))) };
+      `OK proof
+      end
     with e ->
       let (e, info) = Errors.push e in
       (try match Stateid.get info with
@@ -1192,13 +1240,19 @@ end = struct (* {{{ *)
                 spc () ++ iprint (e, info))
     with e ->
       msg_error (str"unable to print error message: " ++
-                    str (Printexc.to_string e))); None
+                    str (Printexc.to_string e)));
+      if drop then `ERROR_ADMITTED else `ERROR
 
   let finish_task name (u,cst,_) d p l i =
-    let bucket = (List.nth l i).Stateid.uuid in
-    match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
-    | None -> exit 1
-    | Some (po,_) ->
+    let { Stateid.uuid = bucket }, drop = List.nth l i in
+    let bucket_name =
+      if bucket < 0 then (assert drop; ", no bucket")
+      else Printf.sprintf ", bucket %d" bucket in
+    match check_task_aux bucket_name name l i with
+    | `ERROR -> exit 1
+    | `ERROR_ADMITTED -> u, cst, false
+    | `OK_ADMITTED -> u, cst, false
+    | `OK (po,_) ->
         let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
         let con =
           Nametab.locate_constant
@@ -1225,11 +1279,11 @@ end = struct (* {{{ *)
   
   let check_task name l i =
     match check_task_aux "" name l i with
-    | Some _ -> true
-    | None -> false
+    | `OK _ | `OK_ADMITTED -> true
+    | `ERROR | `ERROR_ADMITTED -> false
 
   let info_tasks l =
-    CList.map_i (fun i { Stateid.loc; name } ->
+    CList.map_i (fun i ({ Stateid.loc; name }, _) ->
       let time1 =
         try float_of_string (Aux_file.get !hints loc "proof_build_time")
         with Not_found -> 0.0 in
@@ -1239,6 +1293,8 @@ end = struct (* {{{ *)
       name, max (time1 +. time2) 0.0001,i) 0 l
 
   let set_perspective idl =
+    ProofTask.set_perspective idl;
+    TaskQueue.broadcast (Option.get !queue);
     let open Stateid in
     let open ProofTask in
     let overlap s1 s2 =
@@ -1254,28 +1310,28 @@ end = struct (* {{{ *)
        BuildProof { t_states = s2 } -> overlap_rel s1 s2
      | _ -> 0)
 
-  let build_proof ~loc ~exn_info ~start ~stop ~name:pname =
+  let build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name:pname =
     let id, valid as t_exn_info = exn_info in
     let cancel_switch = ref false in
     if TaskQueue.n_workers (Option.get !queue) = 0 then
       if !Flags.compilation_mode = Flags.BuildVio then begin
         let f,assign =
-          Future.create_delegate ~blocking:true (State.exn_on id ~valid) in
+         Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
         let task = ProofTask.(BuildProof {
-          t_exn_info; t_start = start; t_stop = stop;
+          t_exn_info; t_start = start; t_stop = stop; t_drop = drop_pt;
           t_assign = assign; t_loc = loc; t_uuid; t_name = pname;
           t_states = VCS.nodes_in_slice ~start ~stop }) in
         TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
         f, cancel_switch
       end else
-        ProofTask.build_proof_here t_exn_info loc stop, cancel_switch
+        ProofTask.build_proof_here ~drop_pt t_exn_info loc stop, cancel_switch
     else 
-      let f, t_assign = Future.create_delegate (State.exn_on id ~valid) in
+      let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
       let t_uuid = Future.uuid f in
       feedback (Feedback.InProgress 1);
       let task = ProofTask.(BuildProof {
-        t_exn_info; t_start = start; t_stop = stop; t_assign;
+        t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt;
         t_loc = loc; t_uuid; t_name = pname;
         t_states = VCS.nodes_in_slice ~start ~stop }) in
       TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
@@ -1286,14 +1342,14 @@ end = struct (* {{{ *)
   let cancel_worker n = TaskQueue.cancel_worker (Option.get !queue) n
 
   (* For external users this name is nicer than request *)
-  type 'a tasks = ('a,VCS.vcs) Stateid.request list
+  type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list
   let dump_snapshot () =
     let tasks = TaskQueue.snapshot (Option.get !queue) in
     let reqs =
       CList.map_filter
         ProofTask.(fun x ->
              match request_of_task `Fresh x with
-             | Some (ReqBuildProof (r, _)) -> Some r
+             | Some (ReqBuildProof (r, b, _)) -> Some(r, b)
              | _ -> None)
         tasks in
     prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs));
@@ -1426,7 +1482,10 @@ end = struct (* {{{ *)
       let goals, _, _, _, _ = Proof.proof p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
-        let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in
+        let f, assign =
+          Future.create_delegate
+            ~name:(Printf.sprintf "subgoal %d" i)
+            (State.exn_on id ~valid:safe_id) in
         let t_ast =
           { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
         let t_name = Goal.uid g in
@@ -1542,18 +1601,20 @@ and Reach : sig
 
 end = struct (* {{{ *)
 
-let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
+let pstate = summary_pstate
 
 let async_policy () =
   let open Flags in
-  if interactive () = `Yes then
-    (async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy)
+  if is_universe_polymorphism () then false
+  else if interactive () = `Yes then
+    (async_proofs_is_master () || !async_proofs_mode = APonLazy)
   else
-    (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff)
+    (!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
 
 let delegate name =
   let time = get_hint_bp_time name in
   time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
+              || !Flags.async_proofs_full
 
 let collect_proof keep cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
@@ -1563,7 +1624,8 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Id.to_string id in
  let loc = (snd cur).loc in
  let is_defined = function
-   | _, { expr = VernacEndProof (Proved (false,_)) } -> true
+   | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } ->
+      true
    | _ -> false in
  let proof_using_ast = function
    | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
@@ -1575,11 +1637,18 @@ let collect_proof keep cur hd brkind id =
  let has_proof_no_using = function
    | Some (_, { expr = VernacProof(_,None) }) -> true
    | _ -> false in
+ let may_pierce_opaque = function
+   | { expr = VernacPrint (PrintName _) } -> true
+   | _ -> false in
  let parent = function Some (p, _) -> p | None -> assert false in
+ let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
+    | (`Sideff (`Ast(x,_)) | `Cmd { cast = x })
+      when may_pierce_opaque x -> `Sync(no_name,None,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
+    | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
     | `Alias _ -> `Sync (no_name,None,`Alias)
     | `Fork((_,_,_,_::_::_), _) ->
@@ -1599,7 +1668,9 @@ let collect_proof keep cur hd brkind id =
           let t, v = proof_no_using last in
           v.expr <- VernacProof(t, Some hint);
           `ASync (parent last,proof_using_ast last,accn,name,delegate name)
-        with Not_found -> `Sync (no_name,None,`NoHint))
+        with Not_found ->
+          let name = name ids in
+          `MaybeASync (parent last, None, accn, name, delegate name))
     | `Fork((_, hd', GuaranteesOpacity, ids), _) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
@@ -1620,22 +1691,34 @@ let collect_proof keep cur hd brkind id =
      else if keep == VtDrop then `Sync (no_name,None,`Aborted)
      else
        let rc = collect (Some cur) [] id in
-       if keep == VtKeep &&
+       if is_empty rc then make_sync `AlreadyEvaluated rc
+       else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
           (not(State.is_cached id) || !Flags.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
 
 let string_of_reason = function
-  | `Transparent -> "Transparent"
-  | `AlreadyEvaluated -> "AlreadyEvaluated"
-  | `Policy -> "Policy"
-  | `NestedProof -> "NestedProof"
-  | `Immediate -> "Immediate"
-  | `Alias -> "Alias"
-  | `NoHint -> "NoHint"
-  | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
-  | `Aborted -> "Aborted"
-  | _ -> "Unknown Reason"
+  | `Transparent -> "non opaque"
+  | `AlreadyEvaluated -> "proof already evaluated"
+  | `Policy -> "policy"
+  | `NestedProof -> "contains nested proof"
+  | `Immediate -> "proof term given explicitly"
+  | `Aborted -> "aborted proof"
+  | `Doesn'tGuaranteeOpacity -> "not a simple opaque lemma"
+  | `MutualProofs -> "block of mutually recursive proofs"
+  | `Alias -> "contains Undo-like command"
+  | `Print -> "contains Print-like command"
+  | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
+  | `Unknown -> "unsupported case"
+
+let log_string s = prerr_debug ("STM: " ^ s)
+let log_processing_async id name = log_string Printf.(sprintf
+  "%s: proof %s: asynch" (Stateid.to_string id) name
+)
+let log_processing_sync id name reason = log_string Printf.(sprintf
+  "%s: proof %s: synch (cause: %s)"
+  (Stateid.to_string id) name (string_of_reason reason)
+)
 
 let wall_clock_last_fork = ref 0.0
 
@@ -1664,7 +1747,7 @@ let known_state ?(redefine_qed=false) ~cache id =
     let step, cache_step, feedback_processed =
       let view = VCS.visit id in
       match view.step with
-      | `Alias id -> (fun () ->
+      | `Alias (id,_) -> (fun () ->
             reach view.next; reach id
           ), cache, true
       | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
@@ -1697,16 +1780,25 @@ let known_state ?(redefine_qed=false) ~cache id =
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
           | `ASync (start, pua, nodes, name, delegate) -> (fun () ->
-                assert(keep == VtKeep);
+                assert(keep == VtKeep || keep == VtKeepAsAxiom);
+                let drop_pt = keep == VtKeepAsAxiom in
                 let stop, exn_info, loc = eop, (id, eop), x.loc in
-                prerr_endline ("Asynchronous " ^ Stateid.to_string id);
+                log_processing_async id name;
                 VCS.create_cluster nodes ~qed:id ~start;
                 begin match brinfo, qed.fproof with
                 | { VCS.kind = `Edit _ }, None -> assert false
-                | { VCS.kind = `Edit _ }, Some (ofp, cancel) ->
+                | { VCS.kind = `Edit (_,_,_, okeep) }, Some (ofp, cancel) ->
                     assert(redefine_qed = true);
+                    if okeep != keep then
+                      msg_error(strbrk("The command closing the proof changed. "
+                        ^"The kernel cannot take this into account and will "
+                        ^(if keep == VtKeep then "not check " else "reject ")
+                        ^"the "^(if keep == VtKeep then "new" else "incomplete")
+                        ^" proof. Reprocess the command declaring "
+                        ^"the proof's statement to avoid that."));
                     let fp, cancel =
-                      Slaves.build_proof ~loc ~exn_info ~start ~stop ~name in
+                      Slaves.build_proof
+                        ~loc ~drop_pt ~exn_info ~start ~stop ~name in
                     Future.replace ofp fp;
                     qed.fproof <- Some (fp, cancel)
                 | { VCS.kind = `Proof _ }, Some _ -> assert false
@@ -1714,9 +1806,11 @@ let known_state ?(redefine_qed=false) ~cache id =
                     reach ~cache:`Shallow start;
                     let fp, cancel =
                       if delegate then
-                        Slaves.build_proof ~loc ~exn_info ~start ~stop ~name
+                        Slaves.build_proof
+                          ~loc ~drop_pt ~exn_info ~start ~stop ~name
                       else
-                        ProofTask.build_proof_here exn_info loc stop, ref false
+                        ProofTask.build_proof_here
+                          ~drop_pt exn_info loc stop, ref false
                     in
                     qed.fproof <- Some (fp, cancel);
                     let proof =
@@ -1734,17 +1828,21 @@ let known_state ?(redefine_qed=false) ~cache id =
                 reach eop; vernac_interp id x; Proof_global.discard_all ()
               ), `Yes, true
           | `Sync (name, pua, reason) -> (fun () ->
-                prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^
-                  string_of_reason reason);
+                log_processing_sync id name reason;
                 reach eop;
                 let wall_clock = Unix.gettimeofday () in
                 record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
                 let proof =
-                  if keep != VtKeep then None
-                  else Some(Proof_global.close_proof
-                              ~keep_body_ucst_sepatate:false
-                              (State.exn_on id ~valid:eop)) in
-                if proof = None then prerr_endline "NONE!!!!!";
+                  match keep with
+                  | VtDrop -> None
+                  | VtKeepAsAxiom ->
+                      let ctx = Evd.empty_evar_universe_context in
+                      let fp = Future.from_val ([],ctx) in
+                      qed.fproof <- Some (fp, ref false); None
+                  | VtKeep ->
+                      Some(Proof_global.close_proof
+                                ~keep_body_ucst_sepatate:false
+                                (State.exn_on id ~valid:eop)) in
                 reach view.next;
                 if keep == VtKeepAsAxiom then
                   Option.iter (vernac_interp id) pua;
@@ -1756,12 +1854,11 @@ let known_state ?(redefine_qed=false) ~cache id =
                 Proof_global.discard_all ()
               ), `Yes, true
           | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
-                prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id);
                 reach ~cache:`Shallow start;
                 (* no sections *)
                 if List.is_empty (Environ.named_context (Global.env ()))
                 then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
-                else pi1 (aux (`Sync (name, pua, `Unknown))) ()
+                else pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
               ), (if redefine_qed then `No else `Yes), true
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
@@ -1818,19 +1915,37 @@ let observe id =
     iraise e
 
 let finish ?(print_goals=false) () =
-  observe (VCS.get_branch_pos (VCS.current_branch ()));
+  let head = VCS.current_branch () in
+  observe (VCS.get_branch_pos head);
   if print_goals then msg_notice (pr_open_cur_subgoals ());
-  VCS.print ()
+  VCS.print ();
+  (* Some commands may by side effect change the proof mode *)
+  match VCS.get_branch head with
+  | { VCS.kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode
+  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+  | _ -> ()
+
 
 let wait () =
   Slaves.wait_all_done ();
   VCS.print ()
 
+let rec join_admitted_proofs id =
+  if Stateid.equal id Stateid.initial then () else
+  let view = VCS.visit id in
+  match view.step with
+  | `Qed ({ keep = VtKeepAsAxiom; fproof = Some (fp,_) },_) ->
+       ignore(Future.force fp);
+       join_admitted_proofs view.next
+  | _ -> join_admitted_proofs view.next
+
 let join () =
   finish ();
   wait ();
   prerr_endline "Joining the environment";
   Global.join_safe_environment ();
+  prerr_endline "Joining Admitted proofs";
+  join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
   VCS.print ()
 
@@ -1863,7 +1978,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
     exit 1
 
-let merge_proof_branch ?id qast keep brname =
+let merge_proof_branch ?valid ?id qast keep brname =
   let brinfo = VCS.get_branch brname in
   let qed fproof = { qast; keep; brname; brinfo; fproof } in
   match brinfo with
@@ -1874,7 +1989,7 @@ let merge_proof_branch ?id qast keep brname =
       VCS.delete_branch brname;
       if keep <> VtDrop then VCS.propagate_sideff None;
       `Ok
-  | { VCS.kind = `Edit (mode, qed_id, master_id) } ->
+  | { VCS.kind = `Edit (mode, qed_id, master_id, _) } ->
       let ofp =
         match VCS.visit qed_id with
         | { step = `Qed ({ fproof }, _) } -> fproof
@@ -1886,7 +2001,7 @@ let merge_proof_branch ?id qast keep brname =
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
-       iraise (State.exn_on Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+       iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
 
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
@@ -1965,11 +2080,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           List.iter (fun b ->
             if not(VCS.Branch.equal b head) then begin
               VCS.checkout b;
-              VCS.commit (VCS.new_node ()) (Alias oid);
+              VCS.commit (VCS.new_node ()) (Alias (oid,x));
             end)
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
-          VCS.commit id (Alias oid);
+          VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
           prerr_endline ("undo to state " ^ Stateid.to_string id);
@@ -1998,7 +2113,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           let queue =
             if !Flags.async_proofs_full then `QueryQueue (ref false)
             else `MainQueue in
-          VCS.commit id (Cmd { cast = x; cids = []; cqueue = queue });
+          VCS.commit id (Cmd {ctac=false;cast = x; cids = []; cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQuery (false,_), VtLater ->
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
@@ -2021,18 +2136,16 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           anomaly(str"VtProofMode must be executed VtNow")
       | VtProofMode mode, VtNow ->
           let id = VCS.new_node ~id:newtip () in
-          VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd {cast = x; cids=[]; cqueue = `MainQueue});
-          VCS.propagate_sideff (Some x);
+          VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue});
           List.iter
             (fun bn -> match VCS.get_branch bn with
             | { VCS.root; kind = `Master; pos } -> ()
             | { VCS.root; kind = `Proof(_,d); pos } ->
                 VCS.delete_branch bn;
                 VCS.branch ~root ~pos bn (`Proof(mode,d))
-            | { VCS.root; kind = `Edit(_,f,q); pos } ->
+            | { VCS.root; kind = `Edit(_,f,q,k); pos } ->
                 VCS.delete_branch bn;
-                VCS.branch ~root ~pos bn (`Edit(mode,f,q)))
+                VCS.branch ~root ~pos bn (`Edit(mode,f,q,k)))
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record ();
@@ -2041,10 +2154,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtProofStep paral, w ->
           let id = VCS.new_node ~id:newtip () in
           let queue = if paral then `TacQueue (ref false) else `MainQueue in
-          VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue });
+          VCS.commit id (Cmd {ctac = true;cast = x;cids = [];cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQed keep, w ->
-          let rc = merge_proof_branch ~id:newtip x keep head in
+          let valid = if tty then Some(VCS.get_branch_pos head) else None in
+          let rc = merge_proof_branch ?valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish ();
           rc
@@ -2056,7 +2170,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtSideff l, w ->
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd { cast = x; cids = l; cqueue = `MainQueue});
+          VCS.commit id (Cmd {ctac=false;cast=x;cids=l;cqueue=`MainQueue});
           VCS.propagate_sideff (Some x);
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -2080,7 +2194,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
-              VCS.commit id (Cmd { cast = x; cids = []; cqueue = `MainQueue});
+              VCS.commit id (Cmd {ctac=false; cast = x; cids = []; cqueue = `MainQueue});
               VCS.propagate_sideff (Some x);
               VCS.checkout_shallowest_proof_branch ();
             end in
@@ -2184,13 +2298,13 @@ let edit_at id =
       | { step = `Sideff (`Ast(_,id)|`Id id) } -> id
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip =
-    let master_id, cancel_switch =
+    let master_id, cancel_switch, keep =
       (* Hum, this should be the real start_id in the clusted and not next *)
       match VCS.visit qed_id with
-      | { step = `Qed ({ fproof = Some (_,cs)},_) } -> start, cs
+      | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
       | _ -> anomaly (str "Cluster not ending with Qed") in
     VCS.branch ~root:master_id ~pos:id
-      VCS.edit_branch (`Edit (mode, qed_id, master_id));
+      VCS.edit_branch (`Edit (mode, qed_id, master_id, keep));
     VCS.delete_cluster_of id;
     cancel_switch := true;
     Reach.known_state ~cache:(interactive ()) id;
@@ -2217,7 +2331,7 @@ let edit_at id =
       let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
       let branch_info =
         match snd (VCS.get_info id).vcs_backup with
-        | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m
+        | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_,_)) }} -> Some m
         | _ -> None in
       match focused, VCS.cluster_of id, branch_info with
       | _, Some _, None -> assert false
@@ -2276,8 +2390,8 @@ let interp verb (_,e as lexpr) =
     let print_goals =
       verb && match clas with
        | VtQuery _, _ -> false
-       | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true
-       | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
+       | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
+       | _ -> not !Flags.coqtop_ui in
     try finish ~print_goals ()
     with e ->
       let e = Errors.push e in
@@ -2328,7 +2442,7 @@ let get_script prf =
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
     | `Sideff (`Id id)  -> find acc id
     | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
-    | `Alias id -> find acc id
+    | `Alias (id,_) -> find acc id
     | `Fork _ -> find acc view.next
     in
   find [] (VCS.get_branch_pos branch)
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 8a62fe79..6fef895a 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -79,7 +79,7 @@ let pop ?(picky=(fun _ -> true)) ?(destroy=ref false)
   Mutex.unlock m;
   x
 
-let signal_destruction { lock = m; cond = c } =
+let broadcast { lock = m; cond = c } =
   Mutex.lock m;
   Condition.broadcast c;
   Mutex.unlock m
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index bc3922b3..7458de51 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -14,7 +14,9 @@ val pop : ?picky:('a -> bool) -> ?destroy:bool ref -> 'a t -> 'a
 val push : 'a t -> 'a -> unit
 val set_order : 'a t -> ('a -> 'a -> int) -> unit
 val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
-val signal_destruction : 'a t -> unit
+
+(* Wake up all waiting threads *)
+val broadcast : 'a t -> unit
 
 (* Non destructive *)
 val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index d71c169d..180f20ae 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -15,7 +15,6 @@ open Bigint
 open Decl_kinds
 open Extend
 open Libnames
-open Flags
 
 let unlock loc =
   let start, stop = Loc.unloc loc in
@@ -118,8 +117,8 @@ let xmlReference ref =
 let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
 let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
 
-let xmlAddLoaPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoaPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
+let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
+let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
 let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
 
 let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
@@ -618,14 +617,17 @@ let rec tmpp v loc =
   | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
   | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
   | VernacNameSectionHypSet _ as x -> xmlTODO loc x
-  | VernacRequire (None,l) ->
-      xmlRequire loc (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some true,l) ->
-      xmlRequire loc ~attr:["export","true"] (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some false,l) ->
-      xmlRequire loc ~attr:["import","true"] (List.map (fun ref ->
+  | VernacRequire (from, import, l) ->
+      let import = match import with
+      | None -> []
+      | Some true -> ["export","true"]
+      | Some false -> ["import","true"]
+      in
+      let from = match from with
+      | None -> []
+      | Some r -> ["from", Libnames.string_of_reference r]
+      in
+      xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
         xmlReference ref) l)
   | VernacImport (true,l) ->
       xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
@@ -665,12 +667,11 @@ let rec tmpp v loc =
 
   (* Auxiliary file and library management *)
   | VernacAddLoadPath (recf,name,None) ->
-      xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name] []
+      xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
   | VernacAddLoadPath (recf,name,Some dp) ->
-      xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name]
+      xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
         [PCData (Names.DirPath.to_string dp)]
-                 
-  | VernacRemoveLoadPath name -> xmlRemoveLoaPath loc ~attr:["path",name] []
+  | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
   | VernacAddMLPath (recf,name) ->
       xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
   | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index e9302bb7..783ff2e1 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -65,6 +65,11 @@ let rec classify_vernac e =
     | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
     | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
       when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
+    (* Univ poly compatibility: we run it now, so that we can just
+     * look at Flags in stm.ml.  Would be nicer to have the stm
+     * look at the entire dag to detect this option. *)
+    | VernacSetOption (["Universe"; "Polymorphism"],_)
+    | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
     (* Stm *)
     | VernacStm Finish -> VtStm (VtFinish, true), VtNow
     | VernacStm Wait -> VtStm (VtWait, true), VtNow
@@ -151,8 +156,8 @@ let rec classify_vernac e =
         let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
         VtSideff ids, VtLater
     | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
+    | VernacBeginSection (_,id) -> VtSideff [id], VtLater
     | VernacUniverse _ | VernacConstraint _
-    | VernacBeginSection _
     | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
     | VernacChdir _ 
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 84df3ecd..b2072221 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -119,7 +119,7 @@ let schedule_vio_compilation j fs =
   let rec filter_argv b = function
     | [] -> []
     | "-schedule-vio2vo" :: rest -> filter_argv true rest
-    | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+    | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest)
     | _ :: rest when b -> filter_argv b rest
     | s :: rest -> s :: filter_argv b rest in
   let prog = Sys.argv.(0) in