aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authormsozeau2006-09-05 12:16:16 +0000
committermsozeau2006-09-05 12:16:16 +0000
commitd2420e3a0716243918dd04cb04a776837366299d (patch)
treeb8e4d0aabc1724cd933dabcbf6fd1dc1837c8226
parentffa32a19398f075e8dc05ebc3b31545eb00e1845 (diff)
Workaround Map.fold semantic change in ocaml-3.08.4 and higher.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9122 85f007b7-540e-0410-9357-904b9bb8a0f7
-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