aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--pretyping/evd.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 7139956411..68eb2d9edc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -46,7 +46,11 @@ type evar_map1 = evar_info Evarmap.t
let empty = Evarmap.empty
-let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let to_list evc = (* Workaround for change in Map.fold behavior *)
+ let l = ref [] in
+ Evarmap.iter (fun ev x -> l:=(ev,x)::!l) evc;
+ !l
+
let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
let find evc k = Evarmap.find k evc
let remove evc k = Evarmap.remove k evc