diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 300b4c8e6..d0cbeb574 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -659,3 +659,6 @@ let pr_evar_defs evd = if evd.metas = Metamap.empty then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd.metas in v 0 (pp_evm ++ cstrs ++ pp_met) + +let pr_metaset metas = + Metaset.fold (fun mv pp -> pr_meta mv ++ pp) metas (Pp.mt()) |