X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=e21f98c27a47fe157d68030f84a5f3d242c4ee2c;hb=da2c7f7bb1d9f27d998e54e09218be2245a00805;hp=0ec8b91756c9e83da6e08d27bf08988dc85e1af3;hpb=a82bb964ad0bf0969dae008a4de854532846e455;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 0ec8b9175..e21f98c27 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -98,8 +98,10 @@ 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
+  | NConstructor (_,None,l) -> "@ " ^
+      String.concat " " (List.map CicNotationPp.pp_term l)
+  | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
+      String.concat " " (List.map CicNotationPp.pp_term l)
   | NCase1 (_,n) -> "*" ^ n ^ ":"
   | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
       " with " ^ CicNotationPp.pp_term wwhat