X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPt.ml;h=cead5e7ae8eda28cc6ec9d5fc8262b522ae6f3b6;hb=2a59f55f4625ebabb02aefc3cb8c8842040be554;hp=90990300abfc6b985bb5266b2ff5800987e53110;hpb=d284dd23d0e12a62a001d3473eadf4942d12ffaa;p=helm.git

diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml
index 90990300a..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
@@ -178,7 +177,7 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list
 type 'term obj =
   | Inductive of 'term capture_variable list * 'term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma
+  | Theorem of NCic.def_flavour * string * 'term * 'term option * NCic.def_pragma
       (** flavour, name, type, body
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage