From bcb1b03d12e321ec7eafcb28844adcc567160e30 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 9 Sep 2017 15:23:21 +0200
Subject: [PATCH] Printing boxes and breaking points for WP.

---
 theories/program_logic/weakestpre.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 2b6cf0f47..23235b3c8 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -40,17 +40,17 @@ Instance: Params (@wp) 5.
 
 Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : uPred_scope.
 Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'WP'  e  {{  Φ  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
 
 Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : uPred_scope.
 Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : uPred_scope.
 
 (* Texan triples *)
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
-- 
GitLab