aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/mlutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/mlutil.ml')
-rw-r--r--plugins/extraction/mlutil.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 1e6a1fffc..22e7080e1 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1005,7 +1005,7 @@ let kill_some_lams bl (ids,c) =
let kill_dummy_lams c =
let ids,c = collect_lams c in
let bl = List.map sign_of_id ids in
- if not (List.mem Keep bl) then raise Impossible;
+ if not (List.memq Keep bl) then raise Impossible;
let rec fst_kill n = function
| [] -> raise Impossible
| Kill _ :: bl -> n