aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-02-04 17:22:36 +0100
committerPierre-Marie Pédrot2019-02-04 17:22:36 +0100
commitc70412ec8b0bb34b7a5607c07d34607a147d834c (patch)
tree0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /plugins/funind/indfun.ml
parent720ee2730684cc289cef588482323d177e0bea59 (diff)
parent191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff)
Merge PR #6914: Primitive integers
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
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) ->