From 1890a2cdc0dcda7335d7f81fc9ce77c0debc4324 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 16:34:56 +0100
Subject: Fixing the classification of Tactic Notation.

---
 tactics/g_ltac.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4
index f46a670080..b55ac9ad06 100644
--- a/tactics/g_ltac.ml4
+++ b/tactics/g_ltac.ml4
@@ -398,8 +398,9 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
   [ TacNonTerm (loc, Names.Id.to_string nt, (p, Option.default "" sep)) ]
 END
 
-VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF
-| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] ->
+VERNAC COMMAND EXTEND VernacTacticNotation
+| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
+  [ VtUnknown, VtNow ] ->
   [
     let l = Locality.LocalityFixme.consume () in
     let n = Option.default 0 n in
-- 
cgit v1.2.3