Keeping track of locations of disambiguated ids and symbols.

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

diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.mli b/matitaB/components/disambiguation/multiPassDisambiguator.mli
index 41e34e09cff74b93c856e0998fd34adb85fe570f..d8e1e3d503a55978193ee7d63109edd8a1358f7f 100644 (file)
--- a/matitaB/components/disambiguation/multiPassDisambiguator.mli
+++ b/matitaB/components/disambiguation/multiPassDisambiguator.mli
@@ -51,7 +51,7 @@ val disambiguate_thing:
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
-  aliases:'alias DisambiguateTypes.Environment.t ->
+  aliases:'alias DisambiguateTypes.InterprEnv.t ->
   universe:GrafiteAst.alias_spec list
     DisambiguateTypes.Environment.t ->
   lookup_in_library:(
@@ -66,7 +66,8 @@ val disambiguate_thing:
    (context: string option list -> 'ast_thing -> Disambiguate.domain) ->
   interpretate_thing:(
     context:'context ->
-    env:'alias DisambiguateTypes.Environment.t ->
+    env:'alias DisambiguateTypes.InterprEnv.t ->
+    universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
     uri:'uri ->
     is_path:bool -> 
     'ast_thing -> 
@@ -81,6 +82,4 @@ val disambiguate_thing:
         ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   string * int * 'ast_thing ->
-  ((DisambiguateTypes.Environment.key * 'alias) list * 
-   'metasenv * 'subst * 'refined_thing * 'ugraph)
-  list * bool
+  ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool