1 files changed, 50 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli
new file mode 100644
index 00000000..9e902126
--- /dev/null
+++ b/contrib/subtac/subtac_cases.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Evd
+open Environ
+open Inductiveops
+open Rawterm
+open Evarutil
+(*i*)
+
+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
+  | NonExhaustive of cases_pattern list
+  | CannotInferPredicate of (constr * types) array
+
+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 Compilation of pattern-matching. *)
+
+module type S = sig
+  val compile_cases :
+    loc ->
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
+    type_constraint -> 
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
+    unsafe_judgment
+end
+
+module Cases_F(C : Coercion.S) : S