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 +++++-
 test-suite/bugs/closed/4316.v | 3 +++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4316.v

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 *)
diff --git a/test-suite/bugs/closed/4316.v b/test-suite/bugs/closed/4316.v
new file mode 100644
index 0000000000..68dec1334a
--- /dev/null
+++ b/test-suite/bugs/closed/4316.v
@@ -0,0 +1,3 @@
+Ltac tac := idtac.
+Reset tac.
+Ltac tac := idtac.
-- 
cgit v1.2.3