aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--pretyping/cases.mli20
1 files changed, 20 insertions, 0 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
new file mode 100644
index 0000000000..c0997c044e
--- /dev/null
+++ b/pretyping/cases.mli
@@ -0,0 +1,20 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Evd
+open Environ
+open Rawterm
+open Evarutil
+(*i*)
+
+(* Compilation of pattern-matching. *)
+
+val compile_multcase :
+ (trad_constraint -> env -> rawconstr -> unsafe_judgment)
+ * 'a evar_defs -> trad_constraint -> env ->
+ rawconstr option * rawconstr list *
+ (identifier list * pattern list * rawconstr) list ->
+ unsafe_judgment