aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarutil.ml')
-rw-r--r--pretyping/evarutil.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 60c4e88bc..f52694edf 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -429,7 +429,7 @@ let rec check_and_clear_in_constr evdref err ids c =
in the type of ev and adjust the source of the dependency *)
let nconcl =
try
- let nids = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) rids Id.Set.empty in
+ let nids = Id.Map.domain rids in
check_and_clear_in_constr evdref (EvarTypingBreak ev) nids (evar_concl evi)
with ClearDependencyError (rid,err) ->
raise (ClearDependencyError (Id.Map.find rid rids,err)) in