]> matita.cs.unibo.it Git - helm.git/commitdiff
removed duplicate entry
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Nov 2005 11:10:19 +0000 (11:10 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Nov 2005 11:10:19 +0000 (11:10 +0000)
helm/ocaml/cic_notation/grafiteParser.ml

index 3ee56c2185d11e14b5c2e773a6a22d9f4fa0785a..f8840cd77a730cf96b1bdf085b6d3b49c3869fd9 100644 (file)
@@ -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 ->