aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.ml')
-rw-r--r--pretyping/pattern.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index be7ebe49cf..2ca7f21e8d 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -39,6 +39,7 @@ type constr_pattern =
(int * bool list * constr_pattern) list (** index of constructor, nb of args *)
| PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
| PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
+ | PInt of Uint63.t
(** Nota : in a [PCase], the array of branches might be shorter than
expected, denoting the use of a final "_ => _" branch *)