X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=e16ce39bd5e5b11ad3901c99455991b48709d762;hp=42d7df86492625b3b8c00340affcce2f5ad995e2;hb=db020b4218272e2e35641ce3bc3b0a9b3afda899;hpb=37ee4577977f031ae897b615784128911450acfa

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index 42d7df864..e16ce39bd 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -86,13 +86,13 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
       String.concat " " (List.map (NotationPp.pp_term status) l)
   | NCase1 (_,n) -> "*" ^ n ^ ":"
-  | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
+  | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^ 
       " with " ^ NotationPp.pp_term status wwhat
   | NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
 (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
   | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
   | NClear (_,l) -> "nclear " ^ String.concat " " l
-  | NDestruct (_,_dom,_skip) -> "ndestruct ..."
+  | NDestruct (_,_dom,_skip) -> "ndestruct ..." 
   | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^
       "...to be implemented..." ^ " " ^ "...to be implemented..."
   | NId _ -> "nid"