X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=c4eacfb5a36d18940f4b04050339e0ffe8e4a484;hb=093f9476ddf96034b89e6ad443f74bcc6c067912;hp=eda934d68bdebadbc5ca4d4ac3d7e8c4d04e143f;hpb=6d66293a79136e2ff290441b19fb18d2f667fed4;p=helm.git

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index eda934d68..c4eacfb5a 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -54,7 +54,7 @@ let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) =
 let rec pp_ntactic status ~map_unicode_to_tex =
  let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
  function
-  | NApply (_,t) -> "napply " ^ NotationPp.pp_term status t
+  | NApply (_,t) -> "@" ^ NotationPp.pp_term status t
   | NSmartApply (_,t) -> "fixme"
   | NAuto (_,(None,flgs)) ->
       "nautobatch" ^
@@ -169,7 +169,7 @@ let pp_ncommand status = function
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"
   | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
-  | NQed (_) -> "nqed"
+  | NQed (_) -> "qed"
   | NCopy (_,name,uri,map) -> 
       "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ 
         String.concat " and "