trace generation with "// by _;"

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 66994a410baa3018fee4c2cf79d7435b0dd557a7..0e79c035d7b0dd9487e71dea28d38e0c0789aa68 100644 (file)
--- 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 ^