diff options
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |