From d0f7823ee36cf443bd1c9632c272b54816599f99 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 30 Jan 2006 23:11:06 +0000
Subject: Gestion des erreurs pour nombre incorrect d'argument des
 constructeurs (et de l'inductif si clause "in I ...")

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

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 7da7abcce6..da9dce2a61 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -23,6 +23,7 @@ type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
   | WrongNumargConstructor of constructor * int
+  | WrongNumargInductive of inductive * int
   | WrongPredicateArity of constr * constr * constr
   | NeedsInversion of constr * constr
   | UnusedClause of cases_pattern list
@@ -31,6 +32,10 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * pattern_matching_error
 
+val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a
+
+val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
+
 (*s Used for old cases in pretyping *)
 
 val branch_scheme : 
-- 
cgit v1.2.3