Skip to content
Snippets Groups Projects
Commit 9d26bad8 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] better pretty-printer with non-closed terms

parent 944bb98c
No related branches found
No related tags found
No related merge requests found
......@@ -801,7 +801,9 @@ struct
else
match Context.get_opt context_pp with
| Some env -> Pretty.pp_term_env env fmt e
| None -> Pretty.pp_term Pretty.empty fmt e
| None ->
let env = Pretty.known Pretty.empty (QED.vars e) in
Pretty.pp_term env fmt e
let pp_pred = pp_term
let pp_var fmt x = pp_term fmt (e_var x)
let pp_vars fmt xs =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment