File: subtac_errors.mli

package info (click to toggle)
coq-doc 8.4pl4-2
  • links: PTS, VCS
  • area: non-free
  • in suites: stretch
  • size: 21,852 kB
  • ctags: 24,335
  • sloc: ml: 140,953; ansic: 1,982; lisp: 1,406; sh: 1,347; makefile: 572; sed: 2
file content (15 lines) | stat: -rw-r--r-- 631 bytes parent folder | download | duplicates (8) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
type term_pp = Pp.std_ppcmds
type subtyping_error =
    UncoercibleInferType of Util.loc * term_pp * term_pp
  | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp
  | UncoercibleRewrite of term_pp * term_pp
type typing_error =
    NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp
  | NonConvertible of Util.loc * term_pp * term_pp
  | NonSigma of Util.loc * term_pp
  | IllSorted of Util.loc * term_pp
exception Subtyping_error of subtyping_error
exception Typing_error of typing_error
exception Debug_msg of string
val typing_error : typing_error -> 'a
val subtyping_error : subtyping_error -> 'a