]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/disambiguate.ml
...
[helm.git] / helm / software / components / disambiguation / disambiguate.ml
index ae56682cef2adbd8fef6ca20c456af16d4e22320..44498d08830b5b7c266f5573739ef119cf772f43 100644 (file)
@@ -379,8 +379,6 @@ let domain_of_obj ~context ast =
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 
-let domain_of_ast_term = domain_of_term;;
-
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)
@@ -406,50 +404,6 @@ let domain_diff dom1 dom2 =
    in
     aux dom1
 
-module type Disambiguator =
-sig
-  val disambiguate_thing:
-    context:'context ->
-    metasenv:'metasenv ->
-    subst:'subst ->
-    use_coercions:bool ->
-    string_context_of_context:('context -> string option list) ->
-    initial_ugraph:'ugraph ->
-    hint: 
-      ('metasenv -> 'raw_thing -> 'raw_thing) * 
-      (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
-         ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
-    mk_implicit:(bool -> 'alias) ->
-    description_of_alias:('alias -> string) ->
-    aliases:'alias DisambiguateTypes.Environment.t ->
-    universe:'alias list DisambiguateTypes.Environment.t option ->
-    lookup_in_library:(
-      DisambiguateTypes.interactive_user_uri_choice_type ->
-      DisambiguateTypes.input_or_locate_uri_type ->
-      DisambiguateTypes.Environment.key ->
-      'alias list) ->
-    uri:'uri ->
-    pp_thing:('ast_thing -> string) ->
-    domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
-    interpretate_thing:(
-      context:'context ->
-      env:'alias DisambiguateTypes.Environment.t ->
-      uri:'uri ->
-      is_path:bool -> 
-      'ast_thing -> 
-      localization_tbl:'cichash -> 
-        'raw_thing) ->
-    refine_thing:(
-      'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
-      'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
-        ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
-    mk_localization_tbl:(int -> 'cichash) ->
-    string * int * 'ast_thing ->
-    ((DisambiguateTypes.Environment.key * 'alias) list * 
-     'metasenv * 'subst * 'refined_thing * 'ugraph)
-    list * bool
-end
-
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
 let disambiguate_thing 
@@ -489,10 +443,7 @@ let disambiguate_thing
               | item -> item
             in
             Environment.find item e
-          with Not_found -> 
-            lookup_in_library 
-              interactive_user_uri_choice 
-              input_or_locate_uri item)
+          with Not_found -> [])
    in
 (*
       (* <benchmark> *)