aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml4
-rw-r--r--engine/evd.mli1
2 files changed, 5 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index b4375d4d6..8f8b29d10 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1026,6 +1026,10 @@ let map_metas_fvalue f evd =
in
set_metas evd (Metamap.smartmap map evd.metas)
+let map_metas f evd =
+ let map cl = map_clb f cl in
+ set_metas evd (Metamap.smartmap map evd.metas)
+
let meta_opt_fvalue evd mv =
match Metamap.find mv evd.metas with
| Clval(_,b,_) -> Some b
diff --git a/engine/evd.mli b/engine/evd.mli
index d43d4f5f9..c8753b9c0 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -451,6 +451,7 @@ val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map
val undefined_metas : evar_map -> metavariable list
val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
+val map_metas : (constr -> constr) -> evar_map -> evar_map
type metabinding = metavariable * constr * instance_status