X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=22e4cbe09e19348aab695521a9947693bcfdaf4a;hb=4b6193be548c96964beee706b75a06e269eed88d;hp=372ab7fb320d498688aaf1457e75e08cc654b076;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 372ab7fb3..22e4cbe09 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -91,9 +91,15 @@ let pp_just ~term_pp =
 
 let pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+  | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
+      assert false ^ " " ^ assert false
+  | NCase1 (_,n) -> "*" ^ n ^ ":"
   | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
       " with " ^ CicNotationPp.pp_term wwhat
+  | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
+      assert false ^ " " ^ assert false
   | NId _ -> "nid"
+  | NIntro (_,n) -> "#" ^ n
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =