diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-25 15:56:57 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-25 15:56:57 +0000 |
| commit | a6a940590b800e38bb0f20143067fd6eb7629e2a (patch) | |
| tree | ca2c1c61bef1f7c072d67ca1ba7e597ce763cc8b /pretyping/reductionops.ml | |
| parent | c3e2a162944063ed8d8308172eff777fecd1ca78 (diff) | |
Fix eta contraction in Reductionops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 29a2b04e0..7d60852fb 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -319,8 +319,8 @@ let rec whd_state_gen flags ts env sigma = let napp = Array.length cl in if napp > 0 then let x', l' = whrec' (array_last cl, empty_stack) in - match kind_of_term x', decomp_stack l' with - | Rel 1, None -> + match kind_of_term x' with + | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in let u = if napp=1 then f else appvect (f,lc) in if noccurn 1 u then (pop u,empty_stack) else s @@ -375,8 +375,8 @@ let local_whd_state_gen flags sigma = let napp = Array.length cl in if napp > 0 then let x', l' = whrec (array_last cl, empty_stack) in - match kind_of_term x', decomp_stack l' with - | Rel 1, None -> + match kind_of_term x' with + | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in let u = if napp=1 then f else appvect (f,lc) in if noccurn 1 u then (pop u,empty_stack) else s |