aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.mli')
-rw-r--r--pretyping/pattern.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index cde6d4dc9..e6ec9a498 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -63,7 +63,7 @@ type extended_patvar_map = (patvar * constr_under_binders) list
type case_info_pattern =
{ cip_style : case_style;
cip_ind : inductive option;
- cip_ind_args : (int * int) option; (** number of params and args *)
+ cip_ind_args : int option; (** number of params and args *)
cip_extensible : bool (** does this match end with _ => _ ? *) }
type constr_pattern =