summaryrefslogtreecommitdiff
path: root/pretyping/pattern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.mli')
-rw-r--r--pretyping/pattern.mli9
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 25a57ed2..1637fc5f 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pattern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: pattern.mli 8755 2006-04-27 22:22:15Z herbelin $ i*)
(*i*)
open Pp
@@ -39,8 +39,9 @@ type constr_pattern =
| PLetIn of name * constr_pattern * constr_pattern
| PSort of rawsort
| PMeta of patvar option
- | PCase of (inductive option * case_style)
- * constr_pattern option * constr_pattern * constr_pattern array
+ | PIf of constr_pattern * constr_pattern * constr_pattern
+ | PCase of (case_style * int array * inductive option * (int * int) option)
+ * constr_pattern * constr_pattern * constr_pattern array
| PFix of fixpoint
| PCoFix of cofixpoint
@@ -76,3 +77,5 @@ val pattern_of_rawconstr : rawconstr ->
val instantiate_pattern :
(identifier * constr_pattern) list -> constr_pattern -> constr_pattern
+
+val lift_pattern : int -> constr_pattern -> constr_pattern