urimanager removed

[helm.git] / matita / components / content / notationPt.ml

diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml
index aa83b20f33cae6066b4a8392e3151901a1a9595b..cead5e7ae8eda28cc6ec9d5fc8262b522ae6f3b6 100644 (file)
--- a/matita/components/content/notationPt.ml
+++ b/matita/components/content/notationPt.ml
@@ -37,7 +37,7 @@ let fail floc msg =
   let (x, y) = HExtlib.loc_of_floc floc in
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
 
-type href = UriManager.uri
+type href = NReference.reference
 
 type child_pos = [ `Left | `Right | `Inner ]
 
@@ -165,7 +165,6 @@ type argument_pattern =
   | IdentArg of int * string (* eta-depth, name *)
 
 type cic_appl_pattern =
-  | UriPattern of UriManager.uri
   | NRefPattern of NReference.reference
   | VarPattern of string
   | ImplicitPattern