work in progress with voids and lveq (was: the most recent voids)

[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 86ede901cdaf5797afe50b50026261d2bbb3cec2..52919dfa1f7cebc3eb38d32de51d97af37a68c2a 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -31,10 +31,11 @@ val disambiguate_term :
   context:Cic.context ->
   metasenv:Cic.metasenv -> 
   subst:Cic.substitution ->
-  ?goal:int ->
+  expty:Cic.term option ->
   ?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 ->