From f57b2e6cf26316ec7df340ab95399039dae5143e Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 18 Jan 2008 17:20:28 +0000
Subject: bug in accessing n-th abstraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10451 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/inv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index d8d7661be7..baa77f9c4b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -117,7 +117,7 @@ let make_inv_predicate env sigma indf realargs id status concl =
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
   in
-  let nhyps = List.length hyps in
+  let nhyps = rel_context_length hyps in
   let env' = push_rel_context hyps env in
   let realargs' = List.map (lift nhyps) realargs in
   let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in
-- 
cgit v1.2.3