aboutsummaryrefslogtreecommitdiff
path: root/checker/declarations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/declarations.ml')
-rw-r--r--checker/declarations.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index d5c34d92b4..94388f4ac1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -39,6 +39,14 @@ type resolver
type substitution = (module_path * resolver option) Umap.t
type 'a subst_fun = substitution -> 'a -> 'a
+let fold_subst fs fb fp =
+ Umap.fold
+ (fun k (mp,_) acc ->
+ match k with
+ MSI msid -> fs msid mp acc
+ | MBI mbid -> fb mbid mp acc
+ | MPI mp1 -> fp mp1 mp acc)
+
let empty_subst = Umap.empty
let add_msid msid mp =