X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdisambiguatingParser.mli;h=5ddf68377f2f2073e406c7049cd978575108f356;hb=9f60b3b0f4460aec52ec241037f6c475b421dd15;hp=6edb842399971bd37f73bd0d20229fc4e7b1371d;hpb=12809955a4a6c693072f5b924603165f83cc382e;p=helm.git diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 6edb84239..5ddf68377 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -25,23 +25,23 @@ exception NoWellTypedInterpretation -module Environment : +module EnvironmentP3 : sig type t - val empty : t + val empty : string val to_string : t -> string val of_string : string -> t end -module Make (C : Disambiguate_types.Callbacks) : +module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : MQIConn.handle -> Cic.context -> Cic.metasenv -> string -> - Environment.t -> (* previous interpretation status *) - Environment.t * (* new interpretation status *) + EnvironmentP3.t -> (* previous interpretation status *) + EnvironmentP3.t * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term (* disambiguated term *) end