diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-10 15:16:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 01:36:22 +0100 |
| commit | a11dd2209f47b6b79ace3d32071d29bd5652e07a (patch) | |
| tree | 11d77d1ccb3b89a6d66cc90f6034761b8f8fbc7a /stm/stm.ml | |
| parent | f63cf9d72c7feb6aa65e525bf6262559a355435f (diff) | |
Relying on Vernac classifier to flag tactics in the STM.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 07262ef68..1d16d99b3 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 |