X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=8a418200d94604127cd7aad3a000aafdca921417;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=bf34fc283d4790c2ffc50244d0828faaacd5bd83;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index bf34fc283..8a418200d 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -660,6 +660,7 @@ EXTEND
 
     nmacro: [
       [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
+      | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
       ]
     ];
     
@@ -802,6 +803,8 @@ EXTEND
         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
+    | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = term -> 
+        G.NInverter (loc,name,indty)
     | NLETCOREC ; defs = let_defs -> 
         nmk_rec_corec `CoInductive defs loc
     | NLETREC ; defs = let_defs ->