New function (only partially implemented) to pretty print an Ast at the

[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 3a8b5213c805484e4bf9b36249244cfe19cfe3d1..7802e582eec59e00a5b6400fce9c3b0e63e8ac5d 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -223,8 +223,8 @@ let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
-  | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
-  | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
+  | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
+  | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term)
   | Alias (_,s) -> pp_alias s
   | Obj (_,obj) -> pp_obj obj
 
@@ -257,3 +257,12 @@ let pp_comment = function
 let pp_statement = function
   | Executable (_, ex) -> pp_executable ex
   | Comment (_, c) -> pp_comment c
+
+let pp_cic_command = function
+  | Include (_,path) -> "include " ^ path
+  | Qed _ -> "qed"
+  | Drop _ -> "drop"
+  | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term)
+  | Set (_, _, _)
+  | Alias (_,_)
+  | Obj (_,_) -> assert false (* not implemented *)