From 4526990e48e179f47ff03fbd61b6640dca2a775c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jun 2018 23:22:07 +0200
Subject: [PATCH] document WP format strings

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

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 9e1ff0076..19934800d 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -52,6 +52,8 @@ Definition wp_eq : @wp = @wp_def := wp_aux.(seal_eq).
 Arguments wp {_ _ _} _ _ _%E _.
 Instance: Params (@wp) 6.
 
+(* Notations without binder -- only parsing because they overlap with the
+notations with binder. *)
 Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
@@ -63,6 +65,9 @@ Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
 Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 
+(* Notations with binder.  The indentation for the inner format block is chosen
+such that *if* one has a single-character mask (e.g. [E]), the second line
+should align with the binder(s) on the first line. *)
 Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' '[          ' @  s ;  E  {{  v ,  Q  } } ']' ']'") : bi_scope.
-- 
GitLab