commented out no longer needed macros Redo, Undo, Abort

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 ->

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index ae9143dabf849ed29f1d9c5c9e41b2f8114c9230..52506019e4b92790e2fdd6290576bd838ba1a9cd 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -99,13 +99,13 @@ type 'term macro =
   | WLocate of loc * string
   | WElim of loc * 'term
   (* real macros *)
-  | Abort of loc
+(*   | Abort of loc *)
   | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
   | Quit of loc
-  | Redo of loc * int option
-  | Undo of loc * int option
+(*   | Redo of loc * int option
+  | Undo of loc * int option *)
 (*   | Print of loc * print_kind *)
   | Search_pat of loc * search_kind * string  (* searches with string pattern *)
   | Search_term of loc * search_kind * 'term  (* searches with term pattern *)

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index eebc73c89c1e1cdb5b01a5ff32c2a02590573af2..a4ec56deecfc3218e69d364211cbce59c7119539 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -120,17 +120,17 @@ let pp_macro pp_term = function
   | WElim (_, t) -> "whelp elim " ^ pp_term t
   | WMatch (_, term) -> "whelp match " ^ pp_term term
   (* real macros *)
-  | Abort _ -> "Abort"
+(*   | Abort _ -> "Abort" *)
   | Check (_, term) -> sprintf "Check %s" (pp_term term)
   | Hint _ -> "hint"
-  | Redo (_, None) -> "Redo"
-  | Redo (_, Some n) -> sprintf "Redo %d" n
+(*   | Redo (_, None) -> "Redo"
+  | Redo (_, Some n) -> sprintf "Redo %d" n *)
   | Search_pat (_, kind, pat) ->
       sprintf "search %s \"%s\"" (pp_search_kind kind) pat
   | Search_term (_, kind, term) ->
       sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
-  | Undo (_, None) -> "Undo"
-  | Undo (_, Some n) -> sprintf "Undo %d" n
+(*   | Undo (_, None) -> "Undo"
+  | Undo (_, Some n) -> sprintf "Undo %d" n *)
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"