diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f4e9aa372..ab83cb15a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -190,7 +190,7 @@ let build_newrecursive l = let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names (loc, gt) = match gt with + let rec lookup names gt = match gt.CAst.v with | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false | GCast(b,_) -> lookup names b |