From 51c078b1cb9e052d32f7f4df3fb70d1fc5968be1 Mon Sep 17 00:00:00 2001
From: coq
Date: Mon, 20 Feb 2006 14:16:36 +0000
Subject: Forgot another file...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8066 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/subtac_errors.ml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 contrib/subtac/subtac_errors.ml

diff --git a/contrib/subtac/subtac_errors.ml b/contrib/subtac/subtac_errors.ml
new file mode 100644
index 0000000000..3bbfe22bc0
--- /dev/null
+++ b/contrib/subtac/subtac_errors.ml
@@ -0,0 +1,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)
-- 
cgit v1.2.3