From a5e0b28f9344744edf2209001fe047b1535775f6 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Apr 2014 12:47:50 +0200
Subject: Fix a small 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 6972f307ba..22ac370b89 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -976,7 +976,7 @@ let rec eta_reduce_head c =
 	(match kind_of_term (eta_reduce_head c') with
            | App (f,cl) ->
                let lastn = (Array.length cl) - 1 in
-               if lastn < 1 then anomaly (Pp.str "application without arguments")
+               if lastn < 0 then anomaly (Pp.str "application without arguments")
                else
                  (match kind_of_term cl.(lastn) with
                     | Rel 1 ->
-- 
cgit v1.2.3