Versions initiales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 0 deletions

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
new file mode 100644
index 000000000..235615498
--- /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