Frontend.DriverMessage
type output_message =
| NormalizedTerm of {
orig : Core.CodeUnit.Syntax.t;
nf : Core.CodeUnit.Syntax.t;
}
| Definition of {
ident : Core.Ident.t;
tp : Core.CodeUnit.Syntax.tp;
ptm : (Core.CodeUnit.Syntax.t * Core.CodeUnit.Syntax.t) option;
}
type error_message =
| LexingError
| ParseError
| UnboundIdent of Core.Ident.t
| InvalidLibrary of string
| UnitNotFound of string
type message =
| OutputMessage of output_message
| WarningMessage of warning_message
| ErrorMessage of {
error : error_message;
last_token : string option;
}
val pp_message : Stdlib.Format.formatter -> message -> unit