From f5e0f609c8c2c77205fcfb296535a7d8856db584 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 15 Sep 2015 15:20:47 +0200
Subject: STM: Reset takes Ltac <ident> into account (Close #4316)

---
 stm/vernac_classifier.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index a2b7795166..8aa2a59177 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -173,9 +173,13 @@ let rec classify_vernac e =
     | VernacDeclareReduction _
     | VernacDeclareClass _ | VernacDeclareInstances _
     | VernacRegister _
-    | VernacDeclareTacticDefinition _
     | VernacNameSectionHypSet _
     | VernacComments _ -> VtSideff [], VtLater
+    | VernacDeclareTacticDefinition (_,l) ->
+        let open Libnames in
+        VtSideff (List.map (function
+          | (Ident (_,r),_,_) -> r
+          | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
-- 
cgit v1.2.3