From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 15 Nov 2005 11:10:19 +0000 (+0000)
Subject: removed duplicate entry
X-Git-Tag: V_0_7_2_3~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0cad23eef95099fd988b666adfbf36bf662432f7;p=helm.git

removed duplicate entry
---

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 3ee56c218..f8840cd77 100644
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -317,7 +317,6 @@ EXTEND
   macro: [
     [ [ IDENT "quit"  ] -> GrafiteAst.Quit loc
 (*     | [ IDENT "abort" ] -> GrafiteAst.Abort loc *)
-    | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
 (*     | [ IDENT "undo"   ]; steps = OPT NUMBER ->
         GrafiteAst.Undo (loc, int_opt steps)
     | [ IDENT "redo"   ]; steps = OPT NUMBER ->