X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.ml;h=9882aa0e92b0335f0aef7467116c87e5c14e9c0a;hb=e42e345f711e051c903072d8cd994ab7b2154b25;hp=f10443c2d01896c004e750b1e3903dba096c27c5;hpb=bc36fe01d5465d07ef76c445c83639e341f3eb2a;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index f10443c2d..9882aa0e9 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -29,6 +29,7 @@ open TacticAst
 
 let tactical_terminator = "."
 let tactic_terminator = tactical_terminator
+let command_terminator = tactical_terminator
 let tactical_separator = ";"
 
 let pp_term_ast term = CicAstPp.pp_term term
@@ -40,6 +41,7 @@ let pp_reduction_kind = function
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
   | `Whd -> "whd"
+  | `Normalize -> "normalize"
 
 let rec pp_tactic = function
   | Absurd (_, term) -> "absurd" ^ pp_term_ast term
@@ -119,17 +121,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"
 
@@ -145,7 +147,7 @@ let pp_alias = function
       sprintf "alias num (instance %d) = \"%s\"" instance desc
   
 let pp_command = function
-  | Qed _ -> "Qed"
+  | Qed _ -> "qed"
   | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
   | Inductive (_, params, types) ->
       let pp_params = function
@@ -204,6 +206,7 @@ and pp_tacticals tacs =
 
 let pp_tactical tac = pp_tactical tac ^ tactical_terminator
 let pp_tactic tac = pp_tactic tac ^ tactic_terminator
+let pp_command tac = pp_command tac ^ command_terminator
 
 let pp_executable = function
   | Macro (_,x) -> pp_macro_ast x