X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=5ac709f9b82fc4e7b5e6dbe6f85fee64abc53570;hb=c8767b56c0a77fa52efb3815524620602709922b;hp=f3ba95765274fcd5788b1dad2112177fa9e49ba8;hpb=2f67829c12dea538114bb848e0275d220dba601b;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index f3ba95765..5ac709f9b 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -408,11 +408,16 @@ 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
   ~initial_ugraph:base_univ ~expty
-  ~mk_implicit ~description_of_alias
+  ~mk_implicit ~description_of_alias ~fix_instance
   ~aliases ~universe ~lookup_in_library 
   ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
   ~mk_localization_tbl
@@ -439,12 +444,7 @@ let disambiguate_thing
             input_or_locate_uri item
       | Some e ->
           (try
-            let item =
-              match item with
-              | Symbol (symb, _) -> Symbol (symb, 0)
-              | item -> item
-            in
-            Environment.find item e
+            fix_instance item (Environment.find item e)
           with Not_found -> [])
    in
 (*