X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=4a94152de956c5ea144f3af78e3ebd6d8392c37a;hb=68a2f8d0a8c34cb7ea0438c7db9222a853a38826;hp=55736e862e2cba8aa5ee548a823691af3f7810aa;hpb=4c3c77a722996633ec810a7fa547f52872124074;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 55736e862..4a94152de 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -182,7 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Quit _ -> "Quit"
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"
@@ -208,6 +207,7 @@ let pp_command ~obj_pp = function
   | Include (_,path) -> "include \"" ^ path ^ "\""
   | Qed _ -> "qed"
   | Drop _ -> "drop"
+  | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
   | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
   | Obj (_,obj) -> obj_pp obj