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

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index f781ea3d7..f10443c2d 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -112,6 +112,13 @@ let pp_search_kind = function
   | `Elim -> "elim"
 
 let pp_macro pp_term = function 
+  (* Whelp *)
+  | WInstance (_, term) -> "whelp instance " ^ pp_term term
+  | WHint (_, t) -> "whelp hint " ^ pp_term t
+  | WLocate (_, s) -> "whelp locate " ^ s
+  | WElim (_, t) -> "whelp elim " ^ pp_term t
+  | WMatch (_, term) -> "whelp match " ^ pp_term term
+  (* real macros *)
   | Abort _ -> "Abort"
   | Check (_, term) -> sprintf "Check %s" (pp_term term)
   | Hint _ -> "hint"
@@ -198,3 +205,15 @@ and pp_tacticals tacs =
 let pp_tactical tac = pp_tactical tac ^ tactical_terminator
 let pp_tactic tac = pp_tactic tac ^ tactic_terminator
 
+let pp_executable = function
+  | Macro (_,x) -> pp_macro_ast x
+  | Tactical (_,x) -> pp_tactical x
+  | Command (_,x) -> pp_command x
+                      
+let pp_comment = function
+  | Note (_,str) -> sprintf "(* %s *)" str
+  | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code)
+
+let pp_statement = function
+  | Executable (_, ex) -> pp_executable ex
+  | Comment (_, c) -> pp_comment c