First commit with new (incomplete) disambiguation engine.

[helm.git] / matitaB / components / disambiguation / multiPassDisambiguator.mli

diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.mli b/matitaB/components/disambiguation/multiPassDisambiguator.mli
index 41b79c9b025b2ea73761cf5937f62be39e841396..41e34e09cff74b93c856e0998fd34adb85fe570f 100644 (file)
--- a/matitaB/components/disambiguation/multiPassDisambiguator.mli
+++ b/matitaB/components/disambiguation/multiPassDisambiguator.mli
@@ -52,8 +52,8 @@ val disambiguate_thing:
   description_of_alias:('alias -> string) ->
   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
-  universe:'alias list
-    DisambiguateTypes.Environment.t option ->
+  universe:GrafiteAst.alias_spec list
+    DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
@@ -61,6 +61,7 @@ val disambiguate_thing:
     'alias list) ->
   uri:'uri ->
   pp_thing:('ast_thing -> string) ->
+  pp_term:(NotationPt.term -> string) -> 
   domain_of_thing:
    (context: string option list -> 'ast_thing -> Disambiguate.domain) ->
   interpretate_thing:(
@@ -75,6 +76,9 @@ val disambiguate_thing:
     'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
     'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> 
       ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
+  visit:(pp_term:(NotationPt.term -> string) -> 
+         (NotationPt.term -> bool) -> 'ast_thing -> 
+        ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   string * int * 'ast_thing ->
   ((DisambiguateTypes.Environment.key * 'alias) list *