Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

27 files changed, 347 insertions, 217 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index e3fb0b607a..c7faef3333 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -60,9 +60,7 @@ module Make(T : Task) = struct
 
   type more_data =
     | MoreDataUnivLevel of Univ.universe_level list
- 
-  let request_expiry_of_task (t, c) = T.request_of_task t, c
-  
+
   let slave_respond (Request r) =
     let res = T.perform r in
     Response res
@@ -125,8 +123,9 @@ module Make(T : Task) = struct
                  "-async-proofs-worker-priority";
                    Flags.string_of_priority !Flags.async_proofs_worker_priority]
         | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile"
-          |"-load-vernac-source" |"-compile-verbose"
+        | ("-async-proofs" |"-toploop" |"-vi2vo"
+          |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
+          |"-compile" |"-compile-verbose"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
           set_slave_opt tl
         | x::tl -> x :: set_slave_opt tl in
@@ -183,6 +182,13 @@ module Make(T : Task) = struct
         let () = Unix.sleep 1 in
         kill_if ()
     in
+    let kill_if () =
+      try kill_if ()
+      with Sys.Break ->
+        let () = stop_waiting := true in
+        let () = TQueue.broadcast queue in
+        Worker.kill proc
+    in
     let _ = Thread.create kill_if () in
 
     try while true do
@@ -297,7 +303,7 @@ module Make(T : Task) = struct
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback fb) []; flush oc in
     Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
-    Pp.log_via_feedback ();
+    Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg));
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with
@@ -313,7 +319,7 @@ module Make(T : Task) = struct
         let response = slave_respond request in
         report_status "Idle";
         marshal_response (Option.get !slave_oc) response;
-        Ephemeron.clear ()
+        CEphemeron.clear ()
       with
       | MarshalError s ->
         pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index a3fe4b8c0d..f140f8ed57 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index c34d447e60..20d5152aac 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 42dd39b927..548958140e 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/dag.ml b/stm/dag.ml
index d0515d3ff1..0c7f9f34bd 100644
--- a/stm/dag.ml
+++ b/stm/dag.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/dag.mli b/stm/dag.mli
index 14ccdc9f1a..6b4442df00 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index df10e7376a..80b3fef196 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -31,6 +31,7 @@ open Reductionops
 open Constrexpr
 open Constrintern
 open Impargs
+open Context.Rel.Declaration
 
 type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
 let mk_hook hook = hook
@@ -44,7 +45,8 @@ let call_hook fix_exn hook l c =
 
 let retrieve_first_recthm = function
   | VarRef id ->
-      (pi2 (Global.lookup_named id),variable_opacity id)
+      let open Context.Named.Declaration in
+      (get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
       (Global.body_of_constant_body cb, is_opaque cb)
@@ -70,11 +72,12 @@ let adjust_guardness_conditions const = function
                   try ignore(Environ.lookup_constant c e); true
                   with Not_found -> false in 
                 if exists c e then e else Environ.add_constant c cb e in
-              let env = Declareops.fold_side_effects (fun env -> function
+              let env = List.fold_left (fun env { eff } ->
+                match eff with
                 | SEsubproof (c, cb,_) -> add c cb env
                 | SEscheme (l,_) ->
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
-                env (Declareops.uniquize_side_effects eff) in
+                env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
 	        search_guard Loc.ghost env
                   possible_indexes fixdecls in
@@ -106,11 +109,12 @@ let find_mutually_recursive_statements thms =
         (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
         (Global.env()) hyps in
       let ind_hyps =
-        List.flatten (List.map_i (fun i (_,b,t) ->
+        List.flatten (List.map_i (fun i decl ->
+          let t = get_type decl in
           match kind_of_term t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
+                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
               [ind,x,i]
           | _ ->
               []) 0 (List.rev whnf_hyp_hds)) in
@@ -185,7 +189,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs pl 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
@@ -204,6 +208,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
            declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           (locality, ConstRef kn) in
     definition_message id;
+    Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r
   with e when Errors.noncritical e ->
     let e = Errors.push e in
@@ -212,17 +217,17 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
 let default_thm_id = Id.of_string "Unnamed_thm"
 
 let compute_proof_name locality = function
-  | Some (loc,id) ->
+  | Some ((loc,id),pl) ->
       (* We check existence here: it's a bit late at Qed time *)
       if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
         user_err_loc (loc,"",pr_id id ++ str " already exists.");
-      id
+      id, pl
   | None ->
-      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 
+      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
 
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
@@ -275,28 +280,28 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named ?export_seff proof =
-  let id,const,cstrs,do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs do_guard persistence hook
+  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+  save ?export_seff id const cstrs pl 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 ?export_seff proof save_ident =
-  let id,const,cstrs,do_guard,persistence,hook = proof in
+  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs do_guard persistence hook
+  save ?export_seff save_ident const cstrs pl do_guard persistence hook
 
 let save_anonymous_with_strength ?export_seff proof kind save_ident =
-  let id,const,cstrs,do_guard,_,hook = proof in
+  let id,const,(cstrs,pl),do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+  save ?export_seff save_ident const cstrs pl do_guard
+      (Global, const.const_entry_polymorphic, Proof kind) hook
 
 (* Admitted *)
 
-let admit (id,k,e) hook () =
+let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
@@ -305,6 +310,7 @@ let admit (id,k,e) hook () =
       str "declared as an axiom.")
   in
   let () = assumption_message id in
+  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
@@ -314,11 +320,10 @@ let set_start_hook = (:=) start_hook
 
 
 let get_proof proof do_guard hook opacity =
-  let (id,(const,cstrs,persistence)) =
+  let (id,(const,univs,persistence)) =
     Pfedit.cook_this_proof proof
   in
-  (** FIXME *)
-  id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
+  id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
 
 let check_exist =
   List.iter (fun (loc,id) ->
@@ -329,16 +334,16 @@ let check_exist =
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in
   make_terminator begin function
-  | Admitted (id,k,pe,ctx) ->
-      admit (id,k,pe) (hook (Some ctx)) ();
+  | Admitted (id,k,pe,(ctx,pl)) ->
+      admit (id,k,pe) pl (hook (Some ctx)) ();
       Pp.feedback Feedback.AddedAxiom
   | 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
+      let proof = get_proof proof compute_guard
+	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
       | Some ((_,id),None) -> save_anonymous ~export_seff proof id
@@ -351,7 +356,7 @@ let universe_proof_terminator compute_guard hook =
 let standard_proof_terminator compute_guard hook =
   universe_proof_terminator compute_guard (fun _ -> hook)
 
-let start_proof id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = match terminator with
   | None -> standard_proof_terminator compute_guard hook
   | Some terminator -> terminator compute_guard hook
@@ -362,9 +367,9 @@ let start_proof id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[])
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
-let start_proof_univs id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = match terminator with
   | None -> universe_proof_terminator compute_guard hook
   | Some terminator -> terminator compute_guard hook
@@ -375,11 +380,11 @@ let start_proof_univs id kind sigma ?terminator ?sign c ?init_tac ?(compute_guar
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun (id,(t,_)) -> (id,t)) thms with
+    match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -387,7 +392,7 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with 
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+    in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
@@ -416,7 +421,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start")
-  | (id,(t,(_,imps)))::other_thms ->
+  | ((id,pl),(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
         | None -> Evd.empty_evar_universe_context
@@ -428,23 +433,27 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
+	    let ctx = UState.context_set (*FIXME*) ctx in
 	    let body = Option.map norm body in
             List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com kind thms hook =
   let env0 = Global.env () in
-  let evdref = ref (Evd.from_env env0) in
+  let levels = Option.map snd (fst (List.hd thms)) in 
+  let evdref = ref (match levels with
+		    | None -> Evd.from_env env0
+		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
+  in
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    check_evars_are_solved env !evdref (Evd.empty,!evdref);
-    let ids = List.map pi1 ctx in
+    evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
+    let ids = List.map get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
        (ids, imps @ lift_implicits (List.length ids) imps'),
@@ -453,8 +462,12 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
-  start_proof_with_initialization kind evd
-    recguard thms snl hook
+  let evd =
+    if pi2 kind then evd
+    else (* We fix the variables to ensure they won't be lowered to Set *)
+      Evd.fix_undefined_variables evd
+  in
+    start_proof_with_initialization kind evd recguard thms snl hook
 
 
 (* Saving a proof *)
@@ -471,14 +484,13 @@ let save_proof ?proof = function
             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
+            let ctx = Evd.evar_context_universe_context (fst universes) in
             Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
         | None ->
             let id, k, typ = Pfedit.current_proof_statement () in
             (* This will warn if the proof is complete *)
             let pproofs, universes =
               Proof_global.return_proof ~allow_partial:true () in
-            let ctx = Evd.evar_context_universe_context universes in
             let sec_vars =
               match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
@@ -488,7 +500,10 @@ let save_proof ?proof = function
                   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),universes)
+	    let names = Pfedit.get_universe_binders () in
+            let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
+		     (universes, Some binders))
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
@@ -507,4 +522,11 @@ let save_proof ?proof = function
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
-    (Evd.empty, Global.env())
+    try (* No more focused goals ? *)
+      let p = Pfedit.get_pftreestate () in
+      let evd = Proof.in_proof p (fun x -> x) in
+      (evd, Global.env ())
+    with Proof_global.NoCurrentProof ->
+      let env = Global.env () in
+      (Evd.from_env env, env)
+           
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index dca6afe19b..9120787d1c 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,12 +9,9 @@
 open Names
 open Term
 open Decl_kinds
-open Constrexpr
-open Vernacexpr
 open Pfedit
 
 type 'a declaration_hook
-
 val mk_hook :
   (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
 
@@ -24,29 +21,31 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
-val start_proof : Id.t -> goal_kind -> Evd.evar_map ->
+val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
   ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
-  (Proof_global.proof_universes option -> unit declaration_hook) -> unit
+  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
 val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-  goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
-  (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
+  goal_kind -> Evd.evar_map ->
+  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  ((Id.t * universe_binders option) *
+     (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
 val universe_proof_terminator :
   Proof_global.lemma_possible_guards ->
-    (Proof_global.proof_universes option -> unit declaration_hook) ->
+    (Evd.evar_universe_context option -> unit declaration_hook) ->
     Proof_global.proof_terminator
 
 val standard_proof_terminator :
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 0e40c345c1..23538a467e 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index c8e6432bb7..fff6d55434 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/spawned.ml b/stm/spawned.ml
index a8372195d4..c6df872679 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -11,7 +11,7 @@ open Spawn
 let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
 let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
 
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
 
 let handshake cin cout =
   try
@@ -26,18 +26,19 @@ let handshake cin cout =
   | End_of_file ->
       pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
 
-let open_bin_connection h p =
+let open_bin_connection h pr pw =
   let open Unix in
-  let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in
+  let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
+  let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) in
   set_binary_mode_in cin true;
   set_binary_mode_out cout true;
   let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in
   cin, cout
 
-let controller h p =
+let controller h pr pw =
   prerr_endline "starting controller thread";
   let main () =
-    let ic, oc = open_bin_connection h p in
+    let ic, oc = open_bin_connection h pr pw in
     let rec loop () =
       try
         match CThread.thread_friendly_input_value ic with
@@ -61,8 +62,8 @@ let init_channels () =
   if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
   let () = match !main_channel with
   | None -> ()
-  | Some (Socket(mh,mp)) ->
-    channels := Some (open_bin_connection mh mp);
+  | Some (Socket(mh,mpr,mpw)) ->
+    channels := Some (open_bin_connection mh mpr mpw);
   | Some AnonPipe ->
     let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
     let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
@@ -74,8 +75,8 @@ let init_channels () =
   in
   match !control_channel with
   | None -> ()
-  | Some (Socket (ch, cp)) ->
-    controller ch cp
+  | Some (Socket (ch, cpr, cpw)) ->
+    controller ch cpr cpw
   | Some AnonPipe ->
     Errors.anomaly (Pp.str "control channel cannot be a pipe")
 
diff --git a/stm/spawned.mli b/stm/spawned.mli
index d9e7baff3b..acad49f379 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (* To link this file, threads are needed *)
 
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
 
 (* Argument parsing should set these *)
 val main_channel : chandescr option ref
diff --git a/stm/stm.ml b/stm/stm.ml
index e6271f6089..92032e9bc3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -51,6 +51,9 @@ let execution_error, execution_error_hook = Hook.make
     feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
+ ~default:(fun _ _ -> ()) ()
+
+let tactic_being_run, tactic_being_run_hook = Hook.make
  ~default:(fun _ -> ()) ()
 
 include Hook
@@ -80,13 +83,25 @@ let async_proofs_workers_extra_env = ref [||]
 type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
 let pr_ast { expr } = pr_vernac expr
 
+(* Commands piercing opaque *)
+let may_pierce_opaque = function
+  | { expr = VernacPrint (PrintName _) } -> true
+  | { expr = VernacExtend (("Extraction",_), _) } -> true
+  | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
+  | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
+  | _ -> false
+
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 let vernac_interp ?proof id ?route { verbose; loc; expr } =
   let rec internal_command = function
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
     | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-    | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
+    | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
     | _ -> false in
   if internal_command expr then begin
     prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
@@ -123,6 +138,10 @@ let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
   with Proof_global.NoCurrentProof -> str""
 
+let update_global_env () =
+  if Proof_global.there_are_pending_proofs () then
+    Proof_global.update_global_env ()
+
 module Vcs_ = Vcs.Make(Stateid)
 type future_proof = Proof_global.closed_proof_output Future.computation
 type proof_mode = string
@@ -135,9 +154,10 @@ type branch_type =
       proof_mode * Stateid.t * Stateid.t  * vernac_qed_type * Vcs_.Branch.t ]
 type cmd_t = {
   ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
+  ceff : bool; (* is a side-effecting command *)
   cast : ast;
   cids : Id.t list;
-  cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
+  cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] }
 type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
 type qed_t = {
   qast : ast;
@@ -166,7 +186,7 @@ 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;
+                       Evd.evar_counter_summary_name;
                        "program-tcc-table" ]
 type state = {
   system : States.state;
@@ -372,7 +392,7 @@ end = struct (* {{{ *)
          (try let n = Hashtbl.find clus c in from::n
          with Not_found -> [from]); true in
     let oc = open_out fname_dot in
-    output_string oc "digraph states {\nsplines=ortho\n";
+    output_string oc "digraph states {\n";
     Dag.iter graph (fun from cf _ l ->
       let c1 = add_to_clus_or_ids from cf in
       List.iter (fun (dest, trans) ->
@@ -424,8 +444,8 @@ end = struct (* {{{ *)
   let reachable id = reachable !vcs id
   let mk_branch_name { expr = x } = Branch.make
     (match x with
-    | VernacDefinition (_,(_,i),_) -> string_of_id i
-    | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i
+    | VernacDefinition (_,((_,i),_),_) -> string_of_id i
+    | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -505,7 +525,10 @@ end = struct (* {{{ *)
     let rec fill id =
       if (get_info id).state = None then fill (Vcs_aux.visit v id).next
       else copy_info_w_state v id in
-    fill stop
+    let v = fill stop in
+    (* We put in the new dag the first state (since Qed shall run on it,
+     * see check_task_aux) *)
+    copy_info_w_state v start
 
   let nodes_in_slice ~start ~stop =
     List.rev (List.map fst (nodes_in_slice ~start ~stop))
@@ -591,6 +614,7 @@ module State : sig
     ?safe_id:Stateid.t ->
     ?redefine:bool -> ?cache:Summary.marshallable ->
     ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
+  val fix_exn_ref : (iexn -> iexn) ref
 
   val install_cached : Stateid.t -> unit
   val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
@@ -614,6 +638,7 @@ end = struct (* {{{ *)
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
    * failed, so the global state may contain garbage *)
   let cur_id = ref Stateid.dummy
+  let fix_exn_ref = ref (fun x -> x)
 
   (* helpers *)
   let freeze_global_state marshallable =
@@ -624,10 +649,9 @@ end = struct (* {{{ *)
     States.unfreeze system; Proof_global.unfreeze proof
 
   (* hack to make futures functional *)
-  let in_t, out_t = Dyn.create "state4future"
   let () = Future.set_freeze
-    (fun () -> in_t (freeze_global_state `No, !cur_id))
-    (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
+    (fun () -> Obj.magic (freeze_global_state `No, !cur_id))
+    (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i)
   
   type frozen_state = state
   type proof_part =
@@ -639,7 +663,7 @@ end = struct (* {{{ *)
     proof,
     Summary.project_summary (States.summary_of_state system) summary_pstate
 
-  let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
+  let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
 
   let is_cached ?(cache=`No) id =
     if Stateid.equal id !cur_id then
@@ -721,7 +745,10 @@ end = struct (* {{{ *)
     try
       prerr_endline("defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
+      let good_id = match safe_id with None -> !cur_id | Some id -> id in
+      fix_exn_ref := exn_on id ~valid:good_id;
       f ();
+      fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
       prerr_endline ("setting cur id to "^str_id);
@@ -730,13 +757,13 @@ end = struct (* {{{ *)
         Hooks.(call state_computed id ~in_cache:false);
       VCS.reached id true;
       if Proof_global.there_are_pending_proofs () then
-        VCS.goals id (Proof_global.get_open_goals ());
+        VCS.goals id (Proof_global.get_open_goals ())
     with e ->
       let (e, info) = Errors.push e in
       let good_id = !cur_id in
       cur_id := Stateid.dummy;
       VCS.reached id false;
-      Hooks.(call unreachable_state id);
+      Hooks.(call unreachable_state id (e, info));
       match Stateid.get info, safe_id with
       | None, None -> iraise (exn_on id ~valid:good_id (e, info))
       | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
@@ -888,9 +915,16 @@ let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
 let get_hint_ctx loc =
   let s = Aux_file.get !hints loc "context_used" in
-  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
-  let ids = List.map (fun id -> Loc.ghost, id) ids in
-  SsExpr (SsSet ids)
+  match Str.split (Str.regexp ";") s with
+  | ids :: _ ->
+      let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
+      let ids = List.map (fun id -> Loc.ghost, id) ids in
+      begin match ids with
+      | [] -> SsEmpty
+      | x :: xs ->
+          List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
+      end
+  | _ -> raise Not_found
 
 let get_hint_bp_time proof_name =
   try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
@@ -1106,9 +1140,10 @@ end = struct (* {{{ *)
   
   let perform_states query =
     if query = [] then [] else
-    let is_tac = function
-      | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
-      | _ -> false in
+    let is_tac e = match classify_vernac e with
+    | VtProofStep _, _ -> true
+    | _ -> false
+    in
     let initial = 
       let rec aux id =
         try match VCS.visit id with { next } -> aux next
@@ -1379,7 +1414,7 @@ and TacTask : sig
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : ast;
+    t_ast      : int * ast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
@@ -1396,7 +1431,7 @@ end = struct (* {{{ *)
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : ast;
+    t_ast      : int * ast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
@@ -1405,7 +1440,7 @@ end = struct (* {{{ *)
     r_state    : Stateid.t;
     r_state_fb : Stateid.t;
     r_document : VCS.vcs option;
-    r_ast      : ast;
+    r_ast      : int * ast;
     r_goal     : Goal.goal;
     r_name     : string }
 
@@ -1449,12 +1484,27 @@ end = struct (* {{{ *)
     | Some { t_kill } -> t_kill ()
     | _ -> ()
  
+  let command_focus = Proof.new_focus_kind ()
+  let focus_cond = Proof.no_cond command_focus
+
   let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
     Option.iter VCS.restore vcs;
     try
       Reach.known_state ~cache:`No id;
       let t, uc = Future.purify (fun () ->
-        vernac_interp r_state_fb r_ast;
+       let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
+       let g = Evd.find sigma0 r_goal in
+       if not (
+         Evarutil.is_ground_term sigma0 Evd.(evar_concl g) &&
+         List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
+                      Evd.(evar_context g))
+       then
+         Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
+           "goals only"))
+       else begin
+        let (i, ast) = r_ast in
+        Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+        vernac_interp r_state_fb ast;
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
@@ -1462,9 +1512,10 @@ end = struct (* {{{ *)
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
               t, Evd.evar_universe_context sigma
-            else Errors.errorlabstrm "Stm" (str"The solution is not ground"))
-        () in
-      RespBuiltSubProof (t,uc) 
+            else Errors.errorlabstrm "Stm" (str"The solution is not ground")
+       end) ()
+     in
+       RespBuiltSubProof (t,uc)
     with e when Errors.noncritical e -> RespError (Errors.print e)
 
   let name_of_task { t_name } = t_name
@@ -1482,12 +1533,11 @@ end = struct (* {{{ *)
   module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
 
   let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
-    let e, etac, time, fail =
+    let e, time, fail =
       let rec find time fail = function
-        | VernacSolve(_,_,re,b) -> re, b, time, fail
-        | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
+        | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
         | VernacFail e -> find time true e
-        | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
+        | _ -> e, time, fail in find false false e in
     Hooks.call Hooks.with_fail fail (fun () ->
     (if time then System.with_time false else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -1499,8 +1549,7 @@ end = struct (* {{{ *)
           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_ast = (i, { verbose; loc; expr = e }) in
         let t_name = Goal.uid g in
         TaskQueue.enqueue_task queue
           ({ t_state = safe_id; t_state_fb = id;
@@ -1577,7 +1626,8 @@ end = struct (* {{{ *)
       vernac_interp r_for { r_what with verbose = true };
       feedback ~state_id:r_for Feedback.Processed     
     with e when Errors.noncritical e ->
-      let msg = string_of_ppcmds (print e) in
+      let e = Errors.push e in
+      let msg = string_of_ppcmds (iprint e) in
       feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
@@ -1599,7 +1649,7 @@ end = struct (* {{{ *)
   let vernac_interp switch prev id q =
     assert(TaskQueue.n_workers (Option.get !queue) > 0);
     TaskQueue.enqueue_task (Option.get !queue)
-      QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch)
+      QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch)
 
   let init () = queue := Some (TaskQueue.create
     (if !Flags.async_proofs_full then 1 else 0))
@@ -1628,7 +1678,7 @@ 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);
  let no_name = "" in
@@ -1650,16 +1700,20 @@ 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 too_complex_to_delegate = function
+   | { expr = (VernacDeclareModule _
+              | VernacDefineModule _
+              | VernacDeclareModuleType _
+              | VernacInclude _) } -> true
+   | { expr =  (VernacRequire _ | VernacImport _) } -> true
+   | ast -> may_pierce_opaque ast 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)
+      when too_complex_to_delegate 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*)
@@ -1745,8 +1799,9 @@ let known_state ?(redefine_qed=false) ~cache id =
   let cherry_pick_non_pstate () =
     Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
     Lib.freeze ~marshallable:`No in
-  let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
-
+  let inject_non_pstate (s,l) =
+    Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
+  in
   let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
     prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
     reach id;
@@ -1766,19 +1821,26 @@ let known_state ?(redefine_qed=false) ~cache id =
       | `Alias (id,_) -> (fun () ->
             reach view.next; reach id
           ), cache, true
+      | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
+            reach view.next), cache, true
       | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
             reach ~cache:`Shallow view.next;
+            Hooks.(call tactic_being_run true); 
             Partac.vernac_interp
-              cancel !Flags.async_proofs_n_tacworkers view.next id x
+              cancel !Flags.async_proofs_n_tacworkers view.next id x;
+            Hooks.(call tactic_being_run false)
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel }
         when Flags.async_proofs_is_master () -> (fun () ->
             reach view.next;
             Query.vernac_interp cancel view.next id x
           ), cache, false
-      | `Cmd { cast = x } -> (fun () ->
-            reach view.next; vernac_interp id x
-          ), cache, true
+      | `Cmd { cast = x; ceff = eff; ctac } -> (fun () ->
+            reach view.next;
+            if ctac then Hooks.(call tactic_being_run true); 
+            vernac_interp id x;
+            if ctac then Hooks.(call tactic_being_run false); 
+	    if eff then update_global_env ()), cache, true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             reach view.next; vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
@@ -1877,7 +1939,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
       | `Sideff (`Ast (x,_)) -> (fun () ->
-            reach view.next; vernac_interp id x;
+            reach view.next; vernac_interp id x; update_global_env ()
           ), cache, true
       | `Sideff (`Id origin) -> (fun () ->
             reach view.next;
@@ -1904,7 +1966,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline "Initialising workers";
+    prerr_endline "Initializing workers";
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
@@ -2126,8 +2188,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           let id = VCS.new_node ~id:newtip () in
           let queue =
             if !Flags.async_proofs_full then `QueryQueue (ref false)
+            else if Flags.(!compilation_mode = BuildVio) &&
+                    VCS.((get_branch head).kind = `Master) &&
+                    may_pierce_opaque x
+                 then `SkipQueue 
             else `MainQueue in
-          VCS.commit id (Cmd {ctac=false;cast = x; cids = []; cqueue = queue });
+          VCS.commit id (Cmd {ctac=false;ceff=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")
@@ -2150,7 +2216,7 @@ 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.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue});
+          VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
           List.iter
             (fun bn -> match VCS.get_branch bn with
             | { VCS.root; kind = `Master; pos } -> ()
@@ -2168,7 +2234,7 @@ 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 {ctac = true;cast = x;cids = [];cqueue = queue });
+          VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQed keep, w ->
           let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2184,7 +2250,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 {ctac=false;cast=x;cids=l;cqueue=`MainQueue});
+          VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
           VCS.propagate_sideff (Some x);
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -2204,11 +2270,16 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
                Proof_global.there_are_pending_proofs ()
             then begin
               let bname = VCS.mk_branch_name x in
-              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
+              let opacity_of_produced_term =
+                match x.expr with
+                | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+                | _ -> Doesn'tGuaranteeOpacity in
+              VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
-              VCS.commit id (Cmd {ctac=false; cast = x; cids = []; cqueue = `MainQueue});
+	      VCS.commit id (Cmd {ctac = false; ceff = true;
+				    cast = x; cids = []; cqueue = `MainQueue});
               VCS.propagate_sideff (Some x);
               VCS.checkout_shallowest_proof_branch ();
             end in
@@ -2297,6 +2368,17 @@ let edit_at id =
       | { step = `Fork _ } -> false
       | { next } -> aux next in
     aux (VCS.get_branch_pos (VCS.current_branch ())) in
+  let rec is_pure_aux id =
+    let view = VCS.visit id in
+    match view.step with
+    | `Cmd _ -> is_pure_aux view.next
+    | `Fork _ -> true
+    | _ -> false in
+  let is_pure id =
+    match (VCS.visit id).step with
+    | `Qed (_,last_step) -> is_pure_aux last_step
+    | _ -> assert false
+  in
   let is_ancestor_of_cur_branch id =
     Vcs_.NodeSet.mem id
       (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
@@ -2307,7 +2389,9 @@ let edit_at id =
   let rec master_for_br root tip =
       if Stateid.equal tip Stateid.initial then tip else
       match VCS.visit tip with
-      | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip
+      | { step = (`Fork _ | `Qed _) } -> tip
+      | { step = `Sideff (`Ast(_,id)) } -> id
+      | { step = `Sideff _ } -> tip
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip old_branch =
     let master_id, cancel_switch, keep =
@@ -2341,7 +2425,8 @@ let edit_at id =
     VCS.delete_cluster_of id;
     VCS.gc ();
     VCS.print ();
-    Reach.known_state ~cache:(interactive ()) id;
+    if not !Flags.async_proofs_full then
+      Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
@@ -2356,7 +2441,7 @@ let edit_at id =
       | _, Some _, None -> assert false
       | false, Some (qed_id,start), Some(mode,bn) ->
           let tip = VCS.cur_tip () in
-          if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch
+          if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
           then reopen_branch start id mode qed_id tip bn
           else backto id (Some bn)
       | true, Some (qed_id,_), Some(mode,bn) ->
@@ -2396,6 +2481,9 @@ let edit_at id =
         VCS.print ();
         iraise (e, info)
 
+let backup () = VCS.backup ()
+let restore d = VCS.restore d
+
 (*********************** TTY API (PG, coqtop, coqc) ***************************)
 (******************************************************************************)
 
@@ -2539,5 +2627,6 @@ let process_error_hook = Hooks.process_error_hook
 let interp_hook = Hooks.interp_hook
 let with_fail_hook = Hooks.with_fail_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
-
+let get_fix_exn () = !State.fix_exn_ref
+let tactic_being_run_hook = Hooks.tactic_being_run_hook
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 1d926e998e..4279921b3b 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -9,6 +9,7 @@
 open Vernacexpr
 open Names
 open Feedback
+open Loc
 
 (** state-transaction-machine interface *)
 
@@ -19,7 +20,7 @@ open Feedback
    The sentence [s] is parsed in the state [ontop].
    If [newtip] is provided, then the returned state id is guaranteed to be
    [newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) ->
+val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) ->
   bool -> edit_id -> string ->
     Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
@@ -35,7 +36,9 @@ val query :
    new document tip, the document between [id] and [fo.stop] has been dropped.
    The portion between [fo.stop] and [fo.tip] has been kept.  [fo.start] is
    just to tell the gui where the editing zone starts, in case it wants to
-   graphically denote it.  All subsequent [add] happen on top of [id]. *)
+   graphically denote it.  All subsequent [add] happen on top of [id].
+   If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
+*)
 type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
 val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 
@@ -49,11 +52,11 @@ val stop_worker : string -> unit
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 
-(* Saves on the dist a .vio corresponding to the current status:
-   - if the worker prool is empty, all tasks are saved
+(* Saves on the disk a .vio corresponding to the current status:
+   - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
-     of the completed tasks is a failuere) *)
+     of the completed tasks is a failure) *)
 val snapshot_vio : DirPath.t -> string -> unit
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
@@ -81,6 +84,10 @@ val set_compilation_hints : string -> unit
 (* Reorders the task queue putting forward what is in the perspective *)
 val set_perspective : Stateid.t list -> unit
 
+type document
+val backup : unit -> document
+val restore : document -> unit
+
 (** workers **************************************************************** **)
 
 module ProofTask : AsyncTaskQueue.Task
@@ -98,9 +105,12 @@ val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
 val parse_error_hook :
   (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val unreachable_state_hook : (Stateid.t -> unit) Hook.t
+val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
+(* called with true before and with false after a tactic explicitly
+ * in the document is run *)
+val tactic_being_run_hook : (bool -> unit) Hook.t
 
 (* Messages from the workers to the master *)
 val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
@@ -117,7 +127,7 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
 (* Adds a new line to the document.  It replaces the core of Vernac.interp.
    [finish] is called as the last bit of this function is the system
    is running interactively (-emacs or coqtop). *)
-val interp : bool -> located_vernac_expr -> unit
+val interp : bool -> vernac_expr located -> unit
 
 (* Queries for backward compatibility *)
 val current_proof_depth : unit -> int
@@ -130,3 +140,4 @@ val process_error_hook : Future.fix_exn Hook.t
 val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
   Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
 val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
+val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 6fef895ae8..ee121c46a2 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -15,6 +15,7 @@ module PriorityQueue : sig
   val pop : ?picky:('a -> bool) -> 'a t -> 'a
   val push : 'a t -> 'a -> unit
   val clear : 'a t -> unit
+  val length : 'a t -> int
 end = struct
   type 'a item = int * 'a
   type 'a rel = 'a item -> 'a item -> int
@@ -38,6 +39,7 @@ end = struct
   let set_rel rel ({ contents = (xs, _) } as t) =
     let rel (_,x) (_,y) = rel x y in
     t := (List.sort rel xs, rel)
+  let length ({ contents = (l, _) }) = List.length l
 end
 
 type 'a t = {
@@ -92,11 +94,29 @@ let push { queue = q; lock = m; cond = c; release } x =
   Condition.broadcast c;
   Mutex.unlock m
 
+let length { queue = q; lock = m } =
+  Mutex.lock m;
+  let n = PriorityQueue.length q in
+  Mutex.unlock m;
+  n
+
 let clear { queue = q; lock = m; cond = c } =
   Mutex.lock m;
   PriorityQueue.clear q;
   Mutex.unlock m
 
+let clear_saving { queue = q; lock = m; cond = c } f =
+  Mutex.lock m;
+  let saved = ref [] in
+  while not (PriorityQueue.is_empty q) do
+    let elem = PriorityQueue.pop q in
+    match f elem with
+    | Some x -> saved := x :: !saved
+    | None -> ()
+  done;
+  Mutex.unlock m;
+  List.rev !saved
+
 let is_empty { queue = q } = PriorityQueue.is_empty q
 
 let destroy tq =
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 7458de510f..27eca12aff 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -22,9 +22,12 @@ val broadcast : 'a t -> unit
 val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
 
 val clear : 'a t -> unit
+val clear_saving : 'a t -> ('a -> 'b option) -> 'b list
 val is_empty : 'a t -> bool
 
 exception BeingDestroyed
 (* Threads blocked in pop can get this exception if the queue is being
  * destroyed *)
 val destroy : 'a t -> unit
+
+val length : 'a t -> int
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index c1a37fed91..d5333d1077 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index aaa6c2c07d..d1d6de9ae8 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,9 +20,6 @@ let unlock loc =
   let start, stop = Loc.unloc loc in
   (string_of_int start, string_of_int stop)
 
-let xmlNoop = (* almost noop  *)
-  PCData ""
-
 let xmlWithLoc loc ename attr xml =
   let start, stop = unlock loc in
   Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
@@ -244,7 +241,7 @@ and pp_local_decl_expr lde = (* don't know what it is for now *)
   match lde with
   | AssumExpr (_, ce) -> pp_expr ce
   | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) =
+and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
   (* inductive_expr *)
   let b,e = Loc.unloc l in
   let location = ["begin", string_of_int b; "end", string_of_int e] in
@@ -273,7 +270,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
     | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
     | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
   Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
+and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
   (* fixpoint_expr *)
   let start, stop = unlock loc in
   let id = Id.to_string id in
@@ -286,7 +283,7 @@ and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
   | Some ce -> [pp_expr ce]
   | None -> []
   end
-and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *)
+and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
   (* Nota: it is like fixpoint_expr without (optid, roe)
    * so could be merged if there is no more differences *)
   let start, stop = unlock loc in
@@ -307,7 +304,13 @@ and pp_cases_pattern_expr cpe =
       xmlApply loc
         (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
           [pp_cases_pattern_expr cpe])
-  | CPatCstr (loc, ref, cpel1, cpel2) ->
+  | CPatCstr (loc, ref, None, cpel2) ->
+      xmlApply loc
+        (xmlOperator "reference"
+           ~attr:["name", Libnames.string_of_reference ref] loc ::
+         [Element ("impargs", [], []);
+          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+  | CPatCstr (loc, ref, Some cpel1, cpel2) ->
       xmlApply loc
         (xmlOperator "reference"
            ~attr:["name", Libnames.string_of_reference ref] loc ::
@@ -347,7 +350,7 @@ and pp_cases_pattern_expr cpe =
       xmlApply loc
         (xmlOperator "delimiter" ~attr:["name", delim] loc ::
           [pp_cases_pattern_expr cpe])
-and pp_case_expr (e, (name, pat)) =
+and pp_case_expr (e, name, pat) =
   match name, pat with
   | None, None -> xmlScrutinee [pp_expr e]
   | Some (loc, name), None ->
@@ -460,7 +463,7 @@ and pp_expr ?(attr=[]) e =
           (return @
            [Element ("scrutinees", [], List.map pp_case_expr cel)] @
            [pp_branch_expr_list bel]))
-  | CRecord (_, _, _) -> assert false
+  | CRecord (_, _) -> assert false
   | CLetIn (loc, (varloc, var), value, body) ->
       xmlApply loc
         (xmlOperator "let" loc ::
@@ -473,7 +476,7 @@ and pp_expr ?(attr=[]) e =
       xmlApply loc
         (xmlOperator "fix" loc ::
            List.flatten (List.map
-             (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d))
+             (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
              fel))
 
 let pp_comment (c) =
@@ -487,12 +490,12 @@ let rec tmpp v loc =
   (* Control *)
   | VernacLoad (verbose,f) ->
       xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
-  | VernacTime l ->
+  | VernacTime (loc,e) ->
       xmlApply loc (Element("time",[],[]) ::
-                    List.map (fun(loc,e) ->tmpp e loc) l)
-  | VernacRedirect (s, l) ->
+                    [tmpp e loc])
+  | VernacRedirect (s, (loc,e)) ->
       xmlApply loc (Element("redirect",["path", s],[]) ::
-                      List.map (fun(loc,e) ->tmpp e loc) l)
+                    [tmpp e loc])
   | VernacTimeout (s,e) ->
       xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
                     [tmpp e loc])
@@ -500,9 +503,6 @@ let rec tmpp v loc =
   | VernacError _ -> xmlWithLoc loc "error" [] []
 
   (* Syntax *)
-  | VernacTacticNotation _ as x ->
-      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
   | VernacSyntaxExtension (_, ((_, name), sml)) ->
       let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
       xmlReservedNotation attrs name loc
@@ -513,13 +513,6 @@ let rec tmpp v loc =
       xmlScope loc "delimit" name ~attr:["delimiter",tag] []
   | VernacDelimiters (name,None) ->
       xmlScope loc "undelimit" name ~attr:[] []
-  | VernacBindScope (name,l) ->
-      xmlScope loc "bind" name
-        (List.map (function
-          | ByNotation(loc,name,None) -> xmlNotation [] name loc []
-          | ByNotation(loc,name,Some d) ->
-              xmlNotation ["delimiter",d] name loc []
-          | AN ref -> xmlReference ref) l)
   | VernacInfix (_,((_,name),sml),ce,sn) ->
       let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
       let sc_attr =
@@ -535,12 +528,13 @@ let rec tmpp v loc =
         | Some scope -> ["scope", scope]
         | None -> [] in
       xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
+  | VernacBindScope _ as x -> xmlTODO loc x
   | VernacNotationAddFormat _ as x -> xmlTODO loc x
   | VernacUniverse _
   | VernacConstraint _
   | VernacPolymorphic (_, _) as x -> xmlTODO loc x
   (* Gallina *)
-  | VernacDefinition (ldk, (_,id), de) ->
+  | VernacDefinition (ldk, ((_,id),_), de) ->
       let l, dk =
         match ldk with
         | Some l, dk -> (l, dk)
@@ -555,7 +549,7 @@ let rec tmpp v loc =
       let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
       let str_id = Id.to_string id in
       (xmlDef str_dk str_id loc [pp_expr e])
-  | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) ->
+  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
       let str_tk = Kindops.string_of_theorem_kind tk in
       let str_id = Id.to_string id in
       (xmlThm str_tk str_id loc [pp_expr statement])
@@ -575,10 +569,11 @@ let rec tmpp v loc =
       end
   | VernacExactProof _ as x -> xmlTODO loc x
   | VernacAssumption ((l, a), _, sbwcl) ->
+      let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
       let many =
-        List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in
+        List.length (List.flatten (List.map fst binders)) > 1 in
       let exprs =
-        List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in
+        List.flatten (List.map pp_simple_binder binders) in
       let l = match l with Some x -> x | None -> Decl_kinds.Global in
       let kind = string_of_assumption_kind l a many in
       xmlAssumption kind loc exprs
@@ -667,7 +662,7 @@ let rec tmpp v loc =
 
   (* Solving *)
 
-  | (VernacSolve _ | VernacSolveExistential _) as x ->
+  | (VernacSolveExistential _) as x ->
       xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
 
   (* Auxiliary file and library management *)
@@ -693,7 +688,6 @@ let rec tmpp v loc =
   | VernacBackTo _ -> PCData "VernacBackTo"
 
   (* Commands *)
-  | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
   | VernacCreateHintDb _ as x -> xmlTODO loc x
   | VernacRemoveHints _ as x -> xmlTODO loc x
   | VernacHints _ as x -> xmlTODO loc x
@@ -723,7 +717,6 @@ let rec tmpp v loc =
   | VernacRegister _ as x -> xmlTODO loc x
   | VernacComments (cl) ->
       xmlComment loc (List.flatten (List.map pp_comment cl))
-  | VernacNop as x -> xmlTODO loc x
 
   (* Stm backdoor *)
   | VernacStm _ as x -> xmlTODO loc x
diff --git a/stm/texmacspp.mli b/stm/texmacspp.mli
index 58dec8fdc1..858847fb6a 100644
--- a/stm/texmacspp.mli
+++ b/stm/texmacspp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/vcs.ml b/stm/vcs.ml
index dfcbc19ae4..38c029901d 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/vcs.mli b/stm/vcs.mli
index fb79d02cbf..8f22fee843 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2b5eb86834..ecaf0fb7c5 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -60,7 +60,7 @@ let undo_classifier = ref (fun _ -> assert false)
 let set_undo_classifier f = undo_classifier := f
 
 let rec classify_vernac e =
-  let rec static_classifier e = match e with
+  let static_classifier e = match e with
     (* PG compatibility *)
     | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
     | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
@@ -86,7 +86,7 @@ let rec classify_vernac e =
 	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
+    | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
@@ -102,12 +102,10 @@ let rec classify_vernac e =
     | VernacCheckMayEval _ ->
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
-    | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
     | VernacProof _ 
     | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
     | VernacSubproof _ | VernacEndSubproof
-    | VernacSolve _ 
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ -> VtProofStep false, VtLater
@@ -116,36 +114,36 @@ let rec classify_vernac e =
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition (
-       (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) ->
+       (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
         VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
-    | VernacDefinition (_,(_,i),ProveBody _) ->
+    | VernacDefinition (_,((_,i),_),ProveBody _) ->
         VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
     | VernacStartTheoremProof (_,l,_) ->
         let ids = 
-          CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+          CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
         VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
     | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
     | VernacFixpoint (_,l) ->
         let ids, open_proof =
-          List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+          List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
         then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (_,l) ->
         let ids, open_proof =
-          List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+          List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
         then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
-        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
+        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
         VtSideff ids, VtLater    
-    | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
+    | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
     | VernacInductive (_,_,l) ->
-        let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
+        let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
            CList.map_filter (function
@@ -173,7 +171,6 @@ let rec classify_vernac e =
     | VernacDeclareReduction _
     | VernacDeclareClass _ | VernacDeclareInstances _
     | VernacRegister _
-    | VernacDeclareTacticDefinition _
     | VernacNameSectionHypSet _
     | VernacComments _ -> VtSideff [], VtLater
     (* Who knows *)
@@ -191,7 +188,6 @@ let rec classify_vernac e =
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
     | VernacSyntaxExtension _ 
     | VernacSyntacticDefinition _
-    | VernacTacticNotation _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
@@ -204,7 +200,6 @@ let rec classify_vernac e =
     | VernacResetName _ | VernacResetInitial
     | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
     (* What are these? *)
-    | VernacNop
     | VernacToplevelControl _
     | VernacRestoreState _
     | VernacWriteState _ -> VtUnknown, VtNow
@@ -213,13 +208,6 @@ let rec classify_vernac e =
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
-  and classify_vernac_list = function
-    (* spiwack: It would be better to define a monoid on classifiers.
-       So that the classifier of the list would be the composition of
-       the classifier of the individual commands. Currently: special
-       case for singleton lists.*)
-    | [_,c] -> static_classifier c
-    | l -> VtUnknown,VtNow
   in
   let res = static_classifier e in
     if Flags.is_universe_polymorphism () then
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 0680fe8420..45ca5cf6b5 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 4df9603dca..d4dcf72c13 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -43,7 +43,7 @@ let schedule_vio_checking j fs =
   let rec filter_argv b = function
     | [] -> []
     | "-schedule-vio-checking" :: 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 pack = function
@@ -104,9 +104,7 @@ let schedule_vio_compilation j fs =
     let f =
       if Filename.check_suffix f ".vio" then Filename.chop_extension f
       else f in
-    let paths = Loadpath.get_paths () in
-    let _, long_f_dot_v =
-      System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+    let long_f_dot_v = Loadpath.locate_file (f^".v") in
     let aux = Aux_file.load_aux_file_for long_f_dot_v in
     let eta =
       try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli
index e2da502693..c0b6d9e6fa 100644
--- a/stm/vio_checking.mli
+++ b/stm/vio_checking.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index db3bb5ad44..b94fae547d 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index f46303b547..75c325360e 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)