diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index ed5406b79..fa2602789 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -181,7 +181,7 @@ let rec dependent_hyps id idlist sign = let rec dep_rec =function | [] -> [] | (id1::l) -> - let id1ty = snd (lookup_var id1 sign) in + let id1ty = snd (lookup_named id1 sign) in if occur_var id (body_of_type id1ty) then id1::dep_rec l else dep_rec l in dep_rec idlist |