From eec3b87e8cc782cb83ea2eae241129b79c80d496 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 15 Feb 2015 14:07:15 +0100
Subject: Fixing bug #3490.

---
 pretyping/tacred.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9d6eb31b4..91cd08844 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -189,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
              if
 	       Array.for_all (noccurn k) tys
 	       && Array.for_all (noccurn (k+nbfix)) bds
+	       && k <= n
 	     then
 	       (k, List.nth labs (k-1))
 	     else
-- 
cgit v1.2.3