From e9f3791573091038843aa6145801c2d5d2757bd9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 29 Aug 2018 13:04:00 +0200
Subject: [PATCH] change prophecy notation

---
 theories/heap_lang/lib/coin_flip.v | 12 ++++++------
 theories/heap_lang/notation.v      |  3 +--
 theories/program_logic/language.v  |  5 +++--
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 56d18ada3..2bdbab5ce 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -24,11 +24,11 @@ Definition earlyChoice: val :=
 
 Definition lateChoice: val :=
   λ: "x",
-  let: "p" := new prophecy in
+  let: "p" := NewProph in
   "x" <- #0 ;;
       let: "r" := rand #() in
-      resolve "p" to "r" ;;
-              "r".
+      resolve_proph: "p" to: "r" ;;
+      "r".
 
 Section coinflip.
   Context `{!heapG Σ} (N: namespace).
@@ -84,9 +84,9 @@ Section coinflip.
     wp_store.
     iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
     iModIntro. wp_seq. wp_apply rand_spec; try done.
-    iIntros (b') "_". wp_let. wp_bind (resolve _ to _)%E.
-    iApply (wp_resolve_proph with "Hp").
-    iNext. iIntros (->). wp_seq. done.
+    iIntros (b') "_". wp_let.
+    wp_apply (wp_resolve_proph with "Hp").
+    iIntros (->). wp_seq. done.
   Qed.
 
 End coinflip.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 596479602..b94a1a5db 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -158,5 +158,4 @@ Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
 
-Notation "'new' 'prophecy'" := NewProph (at level 100) : expr_scope.
-Notation "'resolve' p 'to' v" := (ResolveProph p v) (at level 100) : expr_scope.
+Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index eeeec847a..7b284d5b2 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -5,8 +5,9 @@ Section language_mixin.
   Context {expr val state observation : Type}.
   Context (of_val : val → expr).
   Context (to_val : expr → option val).
-  (** We annotate the reduction relation with observations [κ], which we will use in the definition
-     of weakest preconditions to keep track of creating and resolving prophecy variables. *)
+  (** We annotate the reduction relation with observations [κ], which we will
+     use in the definition of weakest preconditions to predict future
+     observations and assert correctness of the predictions. *)
   Context (prim_step : expr → state → option observation → expr → state → list expr → Prop).
 
   Record LanguageMixin := {
-- 
GitLab