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

semantics level.

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 *)

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli
index d4cae4405ed66550d4fb159e250d5499bcfce9c1..fb9b45084ee7a584174ee0e2321b9c5a380a5ce1 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.mli
+++ b/helm/ocaml/cic_transformations/tacticAstPp.mli
@@ -35,3 +35,4 @@ val pp_macro_cic: Cic.term TacticAst.macro -> string
 val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string
 val pp_alias: TacticAst.alias_spec -> string
 
+val pp_cic_command: (Cic.term,Cic.obj) TacticAst.command -> string