X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=347eab2dabee8871f938172b44b6da856fc3ef3b;hb=d7f32114f3806b51c2ee483dcb5a86e08d086a72;hp=a33bf6d9de125941874d2de94be0d068d1f55fa3;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index a33bf6d9d..347eab2da 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -91,6 +91,13 @@ let pp_just ~term_pp =
 
 let pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+  | 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 =
@@ -368,11 +375,9 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
       ^ pp_punctuation_tactical punct
   | Tactic (_, None, punct) ->
      pp_punctuation_tactical punct
-  | NTactic (_,Some tac, punct) ->
+  | NTactic (_,tac, punct) ->
      pp_ntactic ~map_unicode_to_tex tac
      ^ pp_punctuation_tactical punct
-  | NTactic (_,None, punct) ->
-     pp_punctuation_tactical punct
   | NonPunctuationTactical (_, tac, punct) ->
      pp_non_punctuation_tactical tac
      ^ pp_punctuation_tactical punct