aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.ml')
-rw-r--r--kernel/environ.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 8a4871a1dc..9b18db78e8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -362,7 +362,7 @@ let insert_after_hyp (ctxt,vals) id d check =
(* To be used in Logic.clear_hyps *)
let remove_hyps ids check_context check_value (ctxt, vals) =
List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) ->
- if List.mem id ids then
+ if Id.Set.mem id ids then
(ctxt,vals)
else
let nd = check_context d in