X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.mli;h=ecb5926820a16be025e14c0f34f80037c2a53d56;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=86ede901cdaf5797afe50b50026261d2bbb3cec2;hpb=9a9c5b863f68367119450ae7b806d454ba1265e3;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
index 86ede901c..ecb592682 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -31,7 +31,7 @@ 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) ->