aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.ml')
-rw-r--r--pretyping/pattern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 105672564..f9dec8f35 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -130,7 +130,7 @@ let pattern_of_constr sigma t =
| Case (ci,p,a,br) ->
let cip = ci.ci_pp_info in
let no = Some (ci.ci_npar,cip.ind_nargs) in
- PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no),
+ PCase ((cip.style,ci.ci_cstr_ndecls,Some ci.ci_ind,no),
pattern_of_constr p,pattern_of_constr a,
Array.map pattern_of_constr br)
| Fix f -> PFix f