Added syntax for ninversion tactic (still experimental).

[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 0db8efc1aa9f2eb020cf8a0d8fdc64e067c58a7d..e022c6f33114c122bac42f2e1ba6e6a99918b3d7 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -118,6 +118,8 @@ let rec pp_ntactic ~map_unicode_to_tex =
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
   | NIntro (_,n) -> "#" ^ n
+  | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^
+      assert false ^ " " ^ assert false
   | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
   | NRewrite (_,dir,n,where) -> "nrewrite " ^
      (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^