X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=83f3a36b6f7a37000c20de0a2996b6a784966e0c;hb=3e068a777bc4bda55d3c7eedc2eb8368e8acb6da;hp=3d6b864926b815ec25f88e9b67262c076be5df65;hpb=b91d9e60b0a5f450d2725d4b9bb3ed7f81ef6d3a;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 3d6b86492..83f3a36b6 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -303,6 +303,7 @@ let pp_arg ~term_pp arg =
   
 let pp_nmacro = function
   | NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term)
+  | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
 ;;
 
 let pp_macro ~term_pp ~lazy_term_pp = 
@@ -370,6 +371,7 @@ let pp_coercion ~term_pp t do_composites arity saturations=
 let pp_ncommand = function
   | UnificationHint (_,t, n) -> 
       "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+  | NInverter (_,_,_,_,_)
   | NObj (_,_)
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"