From a6a940590b800e38bb0f20143067fd6eb7629e2a Mon Sep 17 00:00:00 2001
From: pboutill
Date: Wed, 25 Jul 2012 15:56:57 +0000
Subject: Fix eta contraction in Reductionops

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15650 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 29a2b04e0b..7d60852fb6 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
-- 
cgit v1.2.3