From 8a95a21a90188d8ef4bd790563a63fdf9b4318a9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Sep 2003 19:32:12 +0000
Subject: Correction bug NewInduction pour les inductifs de type 'ordinaux'

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 41dce0fef9..4f9ab4ad18 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1333,7 +1333,9 @@ let compute_induction_names n names =
   names
 
 let is_indhyp p n t =
-  let c,_ = decompose_app t in 
+  let l, c = decompose_prod t in
+  let c,_ = decompose_app c in 
+  let p = p + List.length l in
   match kind_of_term c with
     | Rel k when p < k & k <= p + n -> true
     | _ -> false
-- 
cgit v1.2.3