Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita...

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

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index 42d7df86492625b3b8c00340affcce2f5ad995e2..e16ce39bd5e5b11ad3901c99455991b48709d762 100644 (file)
--- 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"