X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=c8376078285100419e9ba228cadce6fc60170de7;hb=4c2b24a41bec48da2f6b5abc0dda537f12578a87;hp=0e4636d572b15d6c1e31939068887f5947b2078c;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 0e4636d57..c83760782 100644
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -28,7 +28,6 @@
 open Printf
 
 open DisambiguateTypes
-open UriManager
 
 module Ast = NotationPt
 
@@ -408,11 +407,6 @@ let domain_diff dom1 dom2 =
 
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
-type alias_spec =
-  | Ident_alias of string * string        (* identifier, uri *)
-  | Symbol_alias of string * int * string (* name, instance no, description *)
-  | Number_alias of int * string          (* instance no, description *)
-
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context