From 5caebcd8ff2bedae02a23d79251a2344c7aea4d6 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 9 Jun 2007 16:02:11 +0000
Subject: Various Program fixes, multiple pattern matches, aliases. Fix bug in
 coercion code for simultaneous coercion of different arguments of an
 inductive type. Add tactics for dealing with heterogeneous equality. Export
 more error reporting functions from Cases.

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

(limited to 'pretyping')

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 17d74a9fdd..adb66ef475 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -32,10 +32,20 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * pattern_matching_error
 
+val raise_pattern_matching_error : (loc * env * pattern_matching_error) -> 'a
+
 val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a
 
 val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
 
+val error_bad_constructor_loc : loc -> constructor -> inductive -> 'a
+
+val error_bad_pattern_loc : loc -> constructor -> constr -> 'a
+
+val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -> 'a
+
+val error_needs_inversion : env -> constr -> types -> 'a
+
 (*s Compilation of pattern-matching. *)
 
 module type S = sig
-- 
cgit v1.2.3