new tactic constructor: @[n]

[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 89c4e369901fa464e2c15070e93ff04340ededaf..0ec8b91756c9e83da6e08d27bf08988dc85e1af3 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -98,6 +98,8 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
   | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
+  | NConstructor (_,None) -> "@"
+  | NConstructor (_,Some x) -> "@" ^ string_of_int x
   | NCase1 (_,n) -> "*" ^ n ^ ":"
   | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
       " with " ^ CicNotationPp.pp_term wwhat