patch by Brian committed, cut&paste should not crash matita any longer

[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..5f89df9d6ebca083064425ca71598719650905b0 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 ^
@@ -116,7 +116,7 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
 (*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
   | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
-  | NDestruct _ -> "ndestruct"
+  | NDestruct (_,dom,skip) -> "ndestruct ..." 
   | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
   | NId _ -> "nid"