From e50d86c836cf492a637db056b446bb4c70b2e40b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 13:29:12 +0200
Subject: Properly classifying Ltac2 notations.

---
 src/g_ltac2.ml4 | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 20a00afa2e..f558f9b9cc 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -397,8 +397,12 @@ PRINTED BY pr_ltac2entry
 | [ tac2def_syn(e) ] -> [ e ]
 END
 
-VERNAC COMMAND EXTEND VernacDeclareTactic2Definition CLASSIFIED AS SIDEFF
-| [ "Ltac2" ltac2_entry(e) ] -> [
+let classify_ltac2 = function
+| StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow
+| StrVal _ | StrPrm _  | StrTyp _ -> Vernac_classifier.classify_as_sideeff
+
+VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
+| [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [
     let local = Locality.LocalityFixme.consume () in
     Tac2entries.register_struct ?local e
   ]
@@ -433,4 +437,3 @@ open Stdarg
 VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF
 | [ "Print" "Ltac2" reference(tac) ] -> [ Tac2entries.print_ltac tac ]
 END
-
-- 
cgit v1.2.3