X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=5b5b53f52cd8a3b73edc64f35c7cb7670645157a;hb=d96386684e06473c5fbce2707052cf1732831d5c;hp=fa63d1f484e6daca79d910587dafd579fcf5ed15;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index fa63d1f48..5b5b53f52 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -310,7 +310,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                 [] subst in
             [ Node ([loc], Id name, terms) ]))
   | Ast.Uri _ -> []
-  | Ast.Implicit -> []
+  | Ast.NRef _ -> []
+  | Ast.NCic _ -> []
+  | Ast.Implicit _ -> []
   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
   | Ast.Meta (index, local_context) ->
       List.fold_left
@@ -333,7 +335,7 @@ let domain_of_term ~context term =
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
-   | Ast.Theorem (_,_,ty,bo) ->
+   | Ast.Theorem (_,_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []
@@ -406,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
@@ -437,14 +444,25 @@ 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
+
+   (* items with 1 choice are interpreted ASAP *)
+   let aliases, todo_dom = 
+     let rec aux (aliases,acc) = function 
+       | [] -> aliases, acc
+       | (Node (_, item,extra) as node) :: tl -> 
+           let choices = lookup_choices item in
+           if List.length choices <> 1 then aux (aliases, acc@[node]) tl
+           else
+           let tl = tl @ extra in
+           if Environment.mem item aliases then aux (aliases, acc) tl
+           else aux (Environment.add item (List.hd choices) aliases, acc) tl
+     in
+       aux (aliases,[]) todo_dom
+   in
+
 (*
       (* <benchmark> *)
       let _ =