From 9d26bad84ffd9189374f1b4ea1c465af744ac390 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 4 Feb 2019 11:37:33 +0100
Subject: [PATCH] [wp] better pretty-printer with non-closed terms
---
src/plugins/wp/Lang.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index fdcb24f90ac..8577ac6702a 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -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 =
--
GitLab