From 0b4147008092bc08e3188a73426e878cb9a9218d Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Apr 2014 16:38:54 +0200
Subject: Fix a second, trickier, typo in Termops.eta_reduce_head.

---
 pretyping/termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 22ac370b89..741601167d 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -981,7 +981,7 @@ let rec eta_reduce_head c =
                  (match kind_of_term cl.(lastn) with
                     | Rel 1 ->
 			let c' =
-                          if Int.equal lastn 1 then f
+                          if Int.equal lastn 0 then f
 			  else mkApp (f, Array.sub cl 0 lastn)
 			in
 			if noccurn 1 c'
-- 
cgit v1.2.3