diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 310fb1188f..843992f78d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -102,17 +102,17 @@ let pp_transparent_state s = pp (pr_transparent_state s) (* proof printers *) let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_defs evd) -let ppevd evd = pp(pr_evar_defs evd) +let ppevm evd = pp(pr_evar_map evd) +let ppevd evd = pp(pr_evar_map evd) let ppclenv clenv = pp(pr_clenv clenv) let ppgoal g = pp(db_pr_goal g) let pppftreestate p = pp(print_pftreestate p) let pr_gls gls = - hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) + hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) let ppsigmagoal g = pp(pr_goal (sig_it g)) |