From a11dd2209f47b6b79ace3d32071d29bd5652e07a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Mar 2016 15:16:02 +0100
Subject: Relying on Vernac classifier to flag tactics in the STM.

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

diff --git a/stm/stm.ml b/stm/stm.ml
index 07262ef68f..1d16d99b32 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1140,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
-- 
cgit v1.2.3