diff options
| author | Arnaud Spiwack | 2014-04-25 16:38:54 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-04-25 16:39:03 +0200 |
| commit | 0b4147008092bc08e3188a73426e878cb9a9218d (patch) | |
| tree | b4492ce7bcc1b6092724c412f6e3daa9f0e4e2ab | |
| parent | 38d2881dcd1917a93b202c16a55d57d51006ee88 (diff) | |
Fix a second, trickier, typo in Termops.eta_reduce_head.
| -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' |