From 6e9f19b7dc30eb451dc4cb67be0dd202eab22718 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Nov 1999 17:55:44 +0000
Subject: Versions initiales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretype_errors.mli | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 pretyping/pretype_errors.mli

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
new file mode 100644
index 0000000000..2356154989
--- /dev/null
+++ b/pretyping/pretype_errors.mli
@@ -0,0 +1,22 @@
+
+(* $Id$ *)
+
+open Pp
+open Names
+open Term
+open Sign
+open Environ
+open Type_errors
+open Rawterm
+
+(* The type of errors raised by the pretyper *)
+
+exception PreTypeError of loc * path_kind * context * type_error
+
+val error_cant_find_case_type_loc : loc -> unsafe_env -> constr -> 'a
+
+val error_number_branches_loc : 
+  loc -> unsafe_env -> constr -> constr -> int -> 'b
+
+val error_ill_formed_branch_loc : 
+  loc -> path_kind -> unsafe_env -> constr -> int -> constr -> constr -> 'b
-- 
cgit v1.2.3