]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/disambiguate.mli
milestone in basic_2, λδ-2A reconstructed
[helm.git] / helm / software / components / disambiguation / disambiguate.mli
index ffbdf884d17135de2a4ef128ce5ad9fd0fe13c94..cffb1df0aee5d716a93398ca479699ec43498f34 100644 (file)
@@ -96,6 +96,7 @@ val disambiguate_thing:
   expty: 'refined_thing option ->
   mk_implicit:(bool -> 'alias) ->
   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 ->
   lookup_in_library:(