diff options
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index d1d9206fab..2599e2958f 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -273,7 +273,7 @@ and cbv_stack_term info stack env t = (* constructor in a Case -> IOTA *) | (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk))) when red_set (info_flags info) fIOTA -> - let real_args = snd (list_chop ci.ci_npar args) in + let real_args = list_skipn ci.ci_npar args in cbv_stack_term info (stack_app real_args stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) |