summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_errors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac/subtac_errors.ml')
-rw-r--r--contrib/subtac/subtac_errors.ml24
1 files changed, 0 insertions, 24 deletions
diff --git a/contrib/subtac/subtac_errors.ml b/contrib/subtac/subtac_errors.ml
deleted file mode 100644
index 3bbfe22b..00000000
--- a/contrib/subtac/subtac_errors.ml
+++ /dev/null
@@ -1,24 +0,0 @@
-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)