Apply-Silvie tactic added!

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 9038b3b6043a198c12add0c97da8d4c9106ef38b..9e1dffdcd48c226207b7da9ffd718303eb3ad1c2 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -72,6 +72,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   function
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyS (_, term) -> "applyS " ^ term_pp term
   | Auto (_,_,_,Some kind,_) -> "auto " ^ kind
   | Auto _ -> "auto"
   | Assumption _ -> "assumption"