diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 95c58f4cb4ebbe7aae6fc2512d76c322863a3e80..817a21e295c66caeb711b88f17ce6c2d22be4a35 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -6,29 +6,29 @@ Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
   (□ (P → WP e @ E {{ Φ }}))%I.
 Instance: Params (@ht) 4.
 
-Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
+Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e Φ)
+Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ Φ } }" := (True ⊢ ht E P e Φ)
+Notation "{{ P } } e @ E {{ Φ } }" := (True ⊢ ht E P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e Φ)
+Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e%E Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e (λ v, Q))
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : uPred_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P e (λ v, Q))
+Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ v , Q } }" := (True ⊢ ht E P e (λ v, Q))
+Notation "{{ P } } e @ E {{ v , Q } }" := (True ⊢ ht E P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e {{ v , Q } }" := (True ⊢ ht ⊤ P e (λ v, Q))
+Notation "{{ P } } e {{ v , Q } }" := (True ⊢ ht ⊤ P e%E (λ v, Q))
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.