1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
open Util
open Pp
open Printer
type term_pp = Pp.std_ppcmds
type subtyping_error =
| UncoercibleInferType of loc * term_pp * term_pp
| UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp
| UncoercibleRewrite of term_pp * term_pp
type typing_error =
| NonFunctionalApp of loc * term_pp * term_pp * term_pp
| NonConvertible of loc * term_pp * term_pp
| NonSigma of loc * term_pp
| IllSorted of loc * term_pp
exception Subtyping_error of subtyping_error
exception Typing_error of typing_error
exception Debug_msg of string
let typing_error e = raise (Typing_error e)
let subtyping_error e = raise (Subtyping_error e)
|
