new macro ncheck. fixed term2pres for Inductive and LetIn=Cast

[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 27748245654989ef634ad940b51a6b026ec3f6c7..c92e3175f45d9f84d80aa4c88df4272db669a2bb 100644 (file)
--- 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: [