X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=c92e3175f45d9f84d80aa4c88df4272db669a2bb;hb=cf4a3f9226194e0f6dc9572dea1090e2bfa55219;hp=27748245654989ef634ad940b51a6b026ec3f6c7;hpb=d34061fd1c820139fad38c39dee6377e5057bf26;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 277482456..c92e3175f 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -652,6 +652,11 @@ EXTEND
         in
         (params,name,typ,fields)
     ] ];
+
+    nmacro: [
+      [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
+      ]
+    ];
     
     macro: [
       [ [ IDENT "check"   ]; t = term ->
@@ -938,6 +943,7 @@ EXTEND
         punct = punctuation_tactical ->
           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
+    | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
     ]
   ];
   comment: [