aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun.ml')
-rw-r--r--plugins/funind/indfun.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3a04c753ea..d9b0330e2b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -201,7 +201,7 @@ let is_rec names =
let check_id id names = Id.Set.mem id names in
let rec lookup names gt = match DAst.get gt with
| GVar(id) -> check_id id names
- | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
+ | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false
| GCast(b,_) -> lookup names b
| GRec _ -> error "GRec not handled"
| GIf(b,_,lhs,rhs) ->