diff options
| author | glondu | 2009-11-11 20:01:04 +0000 |
|---|---|---|
| committer | glondu | 2009-11-11 20:01:04 +0000 |
| commit | 0601db38b579513e4ab39a161591cd359260490e (patch) | |
| tree | 2741c3b805ec8b890c5b9f58aeb1445ec10590fc /dev | |
| parent | 8556f4e4b5e21535013e6962feabfede6313462b (diff) | |
Promote evar_defs to evar_map (in Evd)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
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)) |