GrafiteAst.Print (unused) removed.

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 1c85b567d48feb17d98064632c60718f4531f15d..834cbcf410f34b9f31379357057526ddceaf62d5 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -362,7 +362,6 @@ EXTEND
         GrafiteAst.WElim (loc, t)
     | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
         GrafiteAst.WHint (loc,t)
-    | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
     ]
   ];
   alias_spec: [