From e5f5ea2da95297fefe1afebfe303c5d5ba7d41aa Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 Jan 2016 15:38:34 +0100
Subject: workers: purge short version of -load-vernac too (fix #4458)

---
 stm/asyncTaskQueue.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index e3fb0b607a..222f02c007 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -125,8 +125,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
-- 
cgit v1.2.3


From d2b468a87cc50b1558feffc6cd3e1b866205c684 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 Jan 2016 16:00:11 +0100
Subject: par: check if the goal is not ground and fail (fix #4465)

---
 stm/stm.ml | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 14142aa0c5..3d007004e2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1471,17 +1471,29 @@ end = struct (* {{{ *)
     try
       Reach.known_state ~cache:`No id;
       let t, uc = Future.purify (fun () ->
+       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 (fun (_,bo,ty) ->
+            Evarutil.is_ground_term sigma0 ty &&
+            Option.cata (Evarutil.is_ground_term sigma0) true bo)
+           Evd.(evar_context g))
+       then
+         Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
+           "goals only"))
+       else begin
         vernac_interp r_state_fb r_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")
         | Evd.Evar_defined t ->
-            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
-- 
cgit v1.2.3


From 08fdf3c7361c75037e12c5cd0e9f965165fed498 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 Jan 2016 21:19:50 +0100
Subject: fixup d2b468a, evar normalization is needed

---
 stm/stm.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 3d007004e2..168d8bf084 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1488,6 +1488,7 @@ end = struct (* {{{ *)
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
         | Evd.Evar_defined t ->
+            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")
-- 
cgit v1.2.3