diff options
| author | msozeau | 2007-06-09 16:02:11 +0000 |
|---|---|---|
| committer | msozeau | 2007-06-09 16:02:11 +0000 |
| commit | 5caebcd8ff2bedae02a23d79251a2344c7aea4d6 (patch) | |
| tree | f10f3e2fb94e16fb5fc6df04e03d79ff428b4bb1 /pretyping | |
| parent | 481b6a29a87d04cfe54607702c83c9d35f371d75 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.mli | 10 |
1 files changed, 10 insertions, 0 deletions
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 |