aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorJim Fehrle2021-03-07 10:15:11 -0800
committerJim Fehrle2021-03-30 09:51:56 -0700
commiteeb142f3c69d2467fbadd7dd1470ac1606b2e5bf (patch)
tree6057d6c11961f6398fcca77313b0e8abcaaa8961 /plugins
parent16d9e9cf378b9eb0ee0fc42c5c0a3a23b3df6ff4 (diff)
Remove the :> type cast
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/glob_termops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 164a446fe3..fb00d2f202 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -342,7 +342,7 @@ let is_free_in id =
| GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false
| GHole _ -> false
| GCast (b, (CastConv t | CastVM t | CastNative t)) ->
- is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b
+ is_free_in b || is_free_in t
| GInt _ | GFloat _ -> false
| GArray (_u, t, def, ty) ->
Array.exists is_free_in t || is_free_in def || is_free_in ty)