From 7b1e94365bee6cc984e5f476864ac753e6f46e3a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 May 2016 13:25:52 +0200
Subject: Pfedit.get_current_context refinement (fix #4523)

Return the most appropriate evar_map for commands that can run on
non-focused proofs (like Check, Show and debug printers) so that
universes and existentials are printed correctly (they are global
to the proof). The API is backwards compatible.
---
 stm/lemmas.ml  | 10 +---------
 stm/lemmas.mli |  1 -
 2 files changed, 1 insertion(+), 10 deletions(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index fb64a10c6c..5b205e79ef 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -509,13 +509,5 @@ let save_proof ?proof = function
 (* Miscellaneous *)
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    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)
+  Pfedit.get_current_context ()
            
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 16e54e318e..ca6af9a3fa 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -60,4 +60,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
-
-- 
cgit v1.2.3


From 34ba7e0d17c76c42a8ece4d195d280f7722f3bae Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 May 2016 13:13:25 +0200
Subject: STM: fix argument filtering for slaves

Command line options to be dropped got outdated after vi -> vio renaming.
This made the par: goal selector do not work in conjunction with -quick.
---
 stm/asyncTaskQueue.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 8649a14c54..1214fc4da9 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -125,7 +125,7 @@ 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"
+        | ("-async-proofs" |"-toploop" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
-- 
cgit v1.2.3