X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaEngine.mli;h=92b2d8e1c1eda89b57cc1a865b2db1633db99dec;hb=a149b1474110583ea5f47fa5bcb85554bba92f19;hp=d5dcddd61e9be5ee7c6a73b83ca0f3c924e1feb7;hpb=134014e54c374789b38b6c53945f63d21ddbacb0;p=helm.git diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index d5dcddd61..92b2d8e1c 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -25,20 +25,19 @@ val eval_ast : ?do_heavy_checks:bool -> - LexiconEngine.status -> GrafiteTypes.status -> string * int * ((CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement) -> - ((GrafiteTypes.status * LexiconEngine.status) * + (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) -exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status +exception EnrichedWithStatus of exn * GrafiteTypes.status (* should be used only by the compiler since it looses the * disambiguation_context (text,prefix_len,_) *) @@ -47,13 +46,12 @@ val eval_from_stream : include_paths:string list -> ?do_heavy_checks:bool -> ?enforce_no_new_aliases:bool -> (* default true *) - ?watch_statuses:(LexiconEngine.status -> GrafiteTypes.status -> unit) -> - LexiconEngine.status -> + ?watch_statuses:(GrafiteTypes.status -> unit) -> GrafiteTypes.status -> Ulexing.lexbuf -> (GrafiteTypes.status -> (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement -> unit) -> - ((GrafiteTypes.status * LexiconEngine.status) * + (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list