improved type hierarchy management

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

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 8e23e56b5357b6e2664e5548e95d5f3660d022d6..9d8d41537fdcbbb198c67a3b031c278a06a82b40 100644 (file)
--- 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