diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index b32a0589052df2bca28a8bebabc5fa7e1b1b7214..25e8c2a8ea5bbebd8c0bb224250a75a6e0ca247f 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -57,6 +57,7 @@ Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
 Arguments wp {_ _} _ _ _.
 Instance: Params (@wp) 4.
 
+(* TODO: On paper, 'wp' is turned into a keyword. *)
 Notation "#> e @ E {{ Φ } }" := (wp E e Φ)
   (at level 20, e, Φ at level 200,
    format "#>  e  @  E  {{  Φ  } }") : uPred_scope.