X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=0399e4ca3c9a00bac560a5c822b376a898d3496d;hb=dba85ad7c7510e7bfd01e5721c63dad528b3e0bf;hp=8e23e56b5357b6e2664e5548e95d5f3660d022d6;hpb=75de1f4c87166f120d8bb42d98926adaf407c98c;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 8e23e56b5..0399e4ca3 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -114,6 +114,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   (* First order tactics *)
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyRule (_, term) -> "apply rule " ^ term_pp term
   | ApplyP (_, term) -> "applyP " ^ term_pp term
   | ApplyS (_, term, params) ->
      "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
@@ -312,6 +313,8 @@ let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
   | Coercion (_, t, do_composites, i, j) ->
      pp_coercion ~term_pp t do_composites i j
+  | UnificationHint (_,t) -> 
+      "unification hint " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""