aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac/subtac_errors.ml
blob: 067da150ec1d546a8e29175b82007311bf0482a8 (plain)
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)