Back-porting from new Matita:

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.mli

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
index ecb5926820a16be025e14c0f34f80037c2a53d56..52919dfa1f7cebc3eb38d32de51d97af37a68c2a 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -35,6 +35,7 @@ val disambiguate_term :
   ?initial_ugraph:CicUniv.universe_graph -> 
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list DisambiguateTypes.Environment.t option ->
@@ -54,6 +55,7 @@ val disambiguate_term :
 val disambiguate_obj :
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list DisambiguateTypes.Environment.t option ->