X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.ml;h=7802e582eec59e00a5b6400fce9c3b0e63e8ac5d;hb=ee8cb3c92bdfd478ed5eefe1735e48dc2dccbed2;hp=3a8b5213c805484e4bf9b36249244cfe19cfe3d1;hpb=9577234cdce1fea3f0090f954f15f897efd2394d;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 3a8b5213c..7802e582e 100644
--- 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 *)