removed debug prerr_endline

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

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index f10443c2d01896c004e750b1e3903dba096c27c5..eebc73c89c1e1cdb5b01a5ff32c2a02590573af2 100644 (file)
--- 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
@@ -145,7 +146,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 +205,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