## prefix is now used for tinycals

[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 f3e3362771feea06e7f34419ffb946d732ed2619..6a493f834a1fe24b6d866c1421741dfa1cc9c809 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -96,6 +96,7 @@ let pp_ntactic ~map_unicode_to_tex = function
   | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
+  | NIntro (_,n) -> n
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =