From 22e1e914e2687a3c0423cb896ceb7c45366975b4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Mar 2016 19:14:29 +0100
Subject: [PATCH] remark on a coq <-> paper difference

---
 program_logic/weakestpre.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index b32a05890..25e8c2a8e 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.
-- 
GitLab