X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=0e79c035d7b0dd9487e71dea28d38e0c0789aa68;hb=a3417bd94b857a7f96a2221ba5b79444823b2144;hp=66994a410baa3018fee4c2cf79d7435b0dd557a7;hpb=5780119aea0a20e74f7c153add432f5d491ee2a5;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 66994a410..0e79c035d 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -98,10 +98,10 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
   | NSmartApply (_,t) -> "fixme"
   | NAuto (_,(None,flgs)) ->
-      "nauto" ^
+      "nautobatch" ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
   | NAuto (_,(Some l,flgs)) ->
-      "nauto" ^ " by " ^
+      "nautobatch" ^ " by " ^
          (String.concat "," (List.map CicNotationPp.pp_term l)) ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
   | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^