- non_punctuational_tacticals ported to NG

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index ecdee9f7bd9a80be1e1dc1909e9595bfa0750c63..547e510253f64302d3f48db36e3ff366074884bc 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -834,6 +834,8 @@ EXTEND
         G.NTactic (loc, G.NId loc, punct)
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
         G.NonPunctuationTactical (loc, tac, punct)
+    | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical ->
+        G.NNonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
     ]
   ];