X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2Finterpretations.ml;h=7e85d0fc1acd7fa061de8137f305b15e77288cc2;hb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;hp=8059eeaaecbac6f3b04497573ff788f1677c61a5;hpb=0d2bfb98d8343b4e6cefdb506a813b7cb5749630;p=helm.git

diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml
index 8059eeaae..7e85d0fc1 100644
--- a/matita/components/content/interpretations.ml
+++ b/matita/components/content/interpretations.ml
@@ -40,7 +40,7 @@ type cic_id = string
 
 type term_info =
   { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
-    uri: (cic_id, UriManager.uri) Hashtbl.t;
+    uri: (cic_id, NReference.reference) Hashtbl.t;
   }
 
   (* persistent state *)
@@ -188,7 +188,7 @@ let remove_interpretation id =
 let init () = List.iter (fun f -> f []) !load_patterns32s
 
 let instantiate_appl_pattern 
-  ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern 
+  ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern 
 =
   let lookup name =
     try List.assoc name env
@@ -197,7 +197,6 @@ let instantiate_appl_pattern
       assert false
   in
   let rec aux = function
-    | Ast.UriPattern uri -> term_of_uri uri
     | Ast.NRefPattern nref -> term_of_nref nref
     | Ast.ImplicitPattern -> mk_implicit false
     | Ast.VarPattern name -> lookup name