From e563ed5bf7681b910e36d2dc4ea99406da940cec Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 May 2000 13:12:16 +0000
Subject: Afficahge des locations

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

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 9944f55a86..8522328977 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -22,6 +22,16 @@ val error_cant_find_case_type_loc :
 val error_ill_formed_branch_loc : 
   loc -> path_kind -> env -> constr -> int -> constr -> constr -> 'b
 
+val error_actual_type_loc :
+  loc -> env -> constr -> constr -> constr -> 'b
+
+val error_cant_apply_not_functional_loc : 
+  loc -> env -> unsafe_judgment -> unsafe_judgment list -> 'b
+
+val error_cant_apply_bad_type_loc : 
+  loc -> env -> int * constr * constr -> 
+      unsafe_judgment -> unsafe_judgment list -> 'b
+
 val error_number_branches_loc : 
   loc -> path_kind -> env -> constr -> constr -> int -> 'b
 
-- 
cgit v1.2.3