1
type term_pp = Pp.std_ppcmds
3
UncoercibleInferType of Util.loc * term_pp * term_pp
4
| UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp
5
| UncoercibleRewrite of term_pp * term_pp
7
NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp
8
| NonConvertible of Util.loc * term_pp * term_pp
9
| NonSigma of Util.loc * term_pp
10
| IllSorted of Util.loc * term_pp
11
exception Subtyping_error of subtyping_error
12
exception Typing_error of typing_error
13
exception Debug_msg of string
14
val typing_error : typing_error -> 'a
15
val subtyping_error : subtyping_error -> 'a