X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=e9209d5154e1faf27474ed193f7120472ebf022f;hb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;hp=59df4ffddb3204e074a3c4366949fc12260fa9ed;hpb=42aa528129728611cae9da02904886522b08f94a;p=helm.git

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 59df4ffdd..e9209d515 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -104,7 +104,7 @@ let rec pp_term ?(pp_parens = true) t =
               sprintf " in %s%s" ty
               (match debug_printing, href_opt with
               | true, Some uri ->
-                  sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+                  sprintf "(i.e.%s)" (NReference.string_of_reference uri)
               | _ -> ""))	  
 	  (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns patterns)
@@ -183,7 +183,7 @@ and pp_pattern =
      let head_pp =
        head ^
        (match debug_printing, href with
-       | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+       | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
        | _ -> "")
      in
      sprintf "%s \\Rightarrow %s"
@@ -347,7 +347,6 @@ let pp_env env =
       env)
 
 let rec pp_cic_appl_pattern = function
-  | Ast.UriPattern uri -> UriManager.string_of_uri uri
   | Ast.NRefPattern nref -> NReference.string_of_reference nref
   | Ast.VarPattern name -> name
   | Ast.ImplicitPattern -> "?"