X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=d4d312bd2b455c38489f81c50ee53e046f1cfd0f;hb=704bbf749f44396c1a610f336b4e1cf0d25e9370;hp=48fc8691c08c37b66a6425d1cd944760c0b24564;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml
index 48fc8691c..d4d312bd2 100644
--- a/matitaB/components/grafite/grafiteAstPp.ml
+++ b/matitaB/components/grafite/grafiteAstPp.ml
@@ -59,7 +59,7 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | NAuto (_,(None,flgs)) ->
       "nautobatch" ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
-  | NAuto (_,(Some l,flgs)) ->
+  | NAuto (_,(Some (_,l),flgs)) ->
       "nautobatch" ^ " by " ^
          (String.concat "," (List.map (NotationPp.pp_term status) l)) ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
@@ -119,13 +119,11 @@ let pp_l2_pattern = NotationPp.pp_term
 
 let pp_alias = function
   | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
-  | Symbol_alias (symb, instance, desc) ->
-      sprintf "alias symbol \"%s\" %s= \"%s\"."
-        symb
-        (if instance=0 then "" else "(instance "^ string_of_int instance ^ ") ")
-        desc
-  | Number_alias (instance,desc) ->
-      sprintf "alias num (instance %d) = \"%s\"." instance desc
+  | Symbol_alias (symb, (* uri *) _, desc) ->
+      sprintf "alias symbol \"%s\" = \"%s\"."
+        symb desc
+  | Number_alias ((* uri *) _,desc) ->
+      sprintf "alias num = \"%s\"." desc
   
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"
@@ -169,7 +167,7 @@ let pp_ncommand status = function
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"
   | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
-  | NQed (_) -> "nqed"
+  | NQed (_,_) -> "nqed"
   | NCopy (_,name,uri,map) -> 
       "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ 
         String.concat " and "