From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 stm/stm.ml | 36 +++++++++++++++++++++++++++++-------
 1 file changed, 29 insertions(+), 7 deletions(-)

(limited to 'stm/stm.ml')

diff --git a/stm/stm.ml b/stm/stm.ml
index 14142aa0..d8b2de4a 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        *)
@@ -53,6 +53,9 @@ let execution_error, execution_error_hook = Hook.make
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
 
+let tactic_being_run, tactic_being_run_hook = Hook.make
+ ~default:(fun _ -> ()) ()
+
 include Hook
 
 (* enables:  Hooks.(call foo args) *)
@@ -1471,6 +1474,18 @@ 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
@@ -1479,9 +1494,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
@@ -1787,16 +1803,21 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), 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; ceff = eff } -> (fun () ->
-            reach view.next; vernac_interp id x;
+      | `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;
@@ -2577,4 +2598,5 @@ 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: *)
-- 
cgit v1.2.3