X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPt.ml;h=cead5e7ae8eda28cc6ec9d5fc8262b522ae6f3b6;hb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;hp=aa83b20f33cae6066b4a8392e3151901a1a9595b;hpb=42aa528129728611cae9da02904886522b08f94a;p=helm.git diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml index aa83b20f3..cead5e7ae 100644 --- 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