From 0af598b77a6242d796c66884477a046448ef1e21 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 01:31:43 +0100 Subject: Moving Tactic Notation to an EXTEND based command. --- stm/vernac_classifier.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'stm/vernac_classifier.ml') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 97d6e1fb7..41b753fb8 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -195,7 +195,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -- cgit v1.2.3