]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/multiPassDisambiguator.mli
arithmetics for λδ
[helm.git] / helm / software / components / disambiguation / multiPassDisambiguator.mli
index a5b5def32df25efaa6eead61293d1970e95d2020..41b79c9b025b2ea73761cf5937f62be39e841396 100644 (file)
@@ -50,6 +50,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 ->