X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdisambiguatingParser.mli;h=a8afd0e65c3a0e23d6846e4b79e75984aacc207b;hb=6b7f04b45232e6c690cacf5815c85c39de1f52b3;hp=5ddf68377f2f2073e406c7049cd978575108f356;hpb=8004125685a99b6c0f2f95fd7f3fa09a4f5c9094;p=helm.git diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 5ddf68377..a8afd0e65 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -36,13 +36,13 @@ module EnvironmentP3 : module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : - MQIConn.handle -> + dbd:Mysql.dbd -> Cic.context -> Cic.metasenv -> string -> EnvironmentP3.t -> (* previous interpretation status *) - EnvironmentP3.t * (* new interpretation status *) - Cic.metasenv * (* new metasenv *) - Cic.term (* disambiguated term *) + (EnvironmentP3.t * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term) list (* disambiguated term *) end