diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 676fc4f3a..b64156649 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -815,6 +815,9 @@ let local_whd_state_gen flags sigma = whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') |args, (Stack.Proj (n,m,p) :: s') -> whrec (Stack.nth args (n+m), s') + |args, (Stack.Fix (f,s',cst)::s'') -> + let x' = Stack.zip(x,args) in + whrec (contract_fix f cst, s' @ (Stack.append_app [|x'|] s'')) |_ -> s else s |