diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d161ce612b..8fe807f2ee 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -370,7 +370,7 @@ let set_pattern_names env ind brv = let arities = Array.map (fun c -> - rel_context_length (fst (decompose_prod_assum c)) - + rel_context_length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in array_map2 (set_names env) arities brv |