diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 139a5d78ba58eef4e2b060849513d94565111ba9..724bfc03381d70628e9b0c44733369939699e4e5 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -89,93 +89,93 @@ Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  ? {{{  x .. y ,   RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  ? {{{  x .. y ,   RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : bi_scope.
+     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
 
 Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
 Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : stdpp_scope.
+     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
 
 Section wp.
 Context `{irisG Λ Σ}.