From 0cad23eef95099fd988b666adfbf36bf662432f7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Nov 2005 11:10:19 +0000 Subject: [PATCH] removed duplicate entry --- helm/ocaml/cic_notation/grafiteParser.ml | 1 - 1 file changed, 1 deletion(-) 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 -> -- 2.39.2