Printing boxes and breaking points for WP.

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 } } }" :=