commented out no longer needed macros Redo, Undo, Abort

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9f5fd193e9d170c05ef4fe9473e175c9805d251d..2f72b23fa4c17ab775ee87df7469ca3578096290 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -469,14 +469,14 @@ EXTEND
       (params, ind_types)
   ] ];
 
-  macro: [[
-      [ IDENT "abort" ] -> TacticAst.Abort loc
-    | [ IDENT "quit"  ] -> TacticAst.Quit loc
+  macro: [
+    [ [ IDENT "quit"  ] -> TacticAst.Quit loc
+(*     | [ IDENT "abort" ] -> TacticAst.Abort loc *)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
-    | [ IDENT "undo"   ]; steps = OPT NUM ->
+(*     | [ IDENT "undo"   ]; steps = OPT NUM ->
         TacticAst.Undo (loc, int_opt steps)
     | [ IDENT "redo"   ]; steps = OPT NUM ->
-        TacticAst.Redo (loc, int_opt steps)
+        TacticAst.Redo (loc, int_opt steps) *)
     | [ IDENT "check"   ]; t = term ->
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
@@ -491,7 +491,8 @@ EXTEND
     | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
         TacticAst.WHint (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
-  ]];
+    ]
+  ];
 
   alias_spec: [
     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->