snapshot (first version in which some extensions work, e.g. infix +)

[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 9fb8455f9260a7aaa3d1d27049a8e5ab99d712ca..f10443c2d01896c004e750b1e3903dba096c27c5 100644 (file)
--- 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"
@@ -125,8 +132,6 @@ let pp_macro pp_term = function
   | Undo (_, Some n) -> sprintf "Undo %d" n
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
-  | Instance _
-  | Match _ -> assert false
 
 let pp_macro_ast = pp_macro pp_term_ast
 let pp_macro_cic = pp_macro pp_term_cic