- we shared the atomic term constructions

[helm.git] / matitaB / components / grafite / grafiteAstPp.ml

diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml
index 48fc8691c08c37b66a6425d1cd944760c0b24564..c4993712754443227cec682337fbbc64567be17f 100644 (file)
--- a/matitaB/components/grafite/grafiteAstPp.ml
+++ b/matitaB/components/grafite/grafiteAstPp.ml
@@ -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"