commented out no longer needed macros Redo, Undo, Abort

[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml

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