diff options
| -rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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' |