diff options
Diffstat (limited to 'pretyping')
| -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 43062a0e8d..afd86420e9 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -310,7 +310,7 @@ and cbv_stack_value info env = function | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) when red_set (info_flags info) fIOTA && Projection.unfolded p -> let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in - cbv_stack_value info env (arg, stk) + cbv_stack_value info env (strip_appl arg stk) (* may be reduced later by application *) | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl) |