From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 27 May 2005 16:52:40 +0000 (+0000)
Subject: commented out no longer needed macros Redo, Undo, Abort
X-Git-Tag: PRE_INDEX_1~109
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c267ae520c0dfd496b6999af2bf0a390b996aaf;p=helm.git

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 9f5fd193e..2f72b23fa 100644
--- 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 ae9143dab..52506019e 100644
--- 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 eebc73c89..a4ec56dee 100644
--- 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"