X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.mli;h=c462af36f9cac05f0028b6eff603892cb3b03f5b;hb=19a25bf176255055193372554437729a6fa1894c;hp=1f5553e912d31875cee67bcd654770c178b1f384;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.mli b/matita/components/ng_disambiguation/grafiteDisambiguate.mli
index 1f5553e91..c462af36f 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.mli
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.mli
@@ -60,7 +60,7 @@ exception BaseUriNotSetYet
 
 val disambiguate_nterm :
  #status as 'status ->
- NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
+ NCic.term NCicRefiner.expected_type -> NCic.context -> NCic.metasenv -> NCic.substitution ->
  NotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * 'status * NCic.term