From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Jul 2005 12:10:00 +0000 (+0000)
Subject: New function (only partially implemented) to pretty print an Ast at the
X-Git-Tag: PRE_GETTER_STORAGE~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee8cb3c92bdfd478ed5eefe1735e48dc2dccbed2;p=helm.git

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 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 *)
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli
index d4cae4405..fb9b45084 100644
--- 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