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.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index c0ef89a712..6f2c241767 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -135,8 +135,9 @@ let pr_existentialset evars =
prlist_with_sep spc pr_evar (Evar.Set.elements evars)
let ppexistentialset evars =
pp (pr_existentialset evars)
-let ppexistentialfilter filter =
- pp (prlist_with_sep spc bool (Evd.Filter.repr filter))
+let ppexistentialfilter filter = match Evd.Filter.repr filter with
+| None -> pp (Pp.str "ΓΈ")
+| Some f -> pp (prlist_with_sep spc bool f)
let ppclenv clenv = pp(pr_clenv clenv)
let ppgoalgoal gl = pp(Goal.pr_goal gl)
let ppgoal g = pp(Printer.pr_goal g)