X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=0fddb21639496a2085b480598c752d6d3099b003;hb=30743ffb0d331aaaa449957238128943ba781ecf;hp=3ab738ab789a579cc41611e42e15bc90f43d22e4;hpb=bf6f5b964bd4e6c16401a4bfab3c29d6824be22a;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 3ab738ab7..0fddb2163 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -91,9 +91,16 @@ let pp_just ~term_pp =
 
 let pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
-  | NChange (_,what,wwhat) -> "nchange " ^ CicNotationPp.pp_term what 
-      ^ " " ^ CicNotationPp.pp_term wwhat
+  | 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
+  | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
@@ -320,10 +327,13 @@ let pp_coercion ~term_pp t do_composites arity saturations=
     
 let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
+  | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri
   | Coercion (_, t, do_composites, i, j) ->
      pp_coercion ~term_pp t do_composites i j
   | PreferCoercion (_,t) -> 
      "prefer coercion " ^ term_pp t
+  | Inverter (_,n,ty,params) ->
+     "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
   | UnificationHint (_,t, n) -> 
       "unification hint " ^ string_of_int n ^ " " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris