matitaprover

[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 fadecd61e9e76825b355cfb2acdb541a436fd129..13ee7297eacec364ab468ce5b29209b36371c7e3 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -467,6 +467,7 @@ EXTEND
       IDENT "set"; n = QSTRING; v = QSTRING ->
         GrafiteAst.Set (loc, n, v)
     | IDENT "drop" -> GrafiteAst.Drop loc
+    | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
     | IDENT "qed" -> GrafiteAst.Qed loc
     | IDENT "variant" ; name = IDENT; SYMBOL ":"; 
       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->