aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 547ca0475a..333cf1a67b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -112,7 +112,8 @@ 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_map evd)
+let ppevm evd = pp(pr_evar_map (Some 2) evd)
+let ppevmall evd = pp(pr_evar_map None evd)
let ppclenv clenv = pp(pr_clenv clenv)
let ppgoalgoal gl = pp(Goal.pr_goal gl)
(* spiwack: deactivated until a replacement is found