aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r--pretyping/evd.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 111cc9d7c..dbcfae0e8 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -44,6 +44,7 @@ let map evc k = Evarmap.find k evc
let rmv evc k = Evarmap.remove k evc
let remap evc k i = Evarmap.add k i evc
let in_dom evc k = Evarmap.mem k evc
+let fold = Evarmap.fold
let add evd ev newinfo = Evarmap.add ev newinfo evd