From a0bc4d00d45d0cc546b55c5920c34d96ea2454e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Nov 2019 16:52:15 +0100
Subject: [PATCH] Fix.

---
 theories/examples/basics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 5ffa5d5..530ccf4 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -171,7 +171,7 @@ Proof.
     by iApply "HΦ".
 Qed.
 
-Lemma prog_fun_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
+Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
   wp_apply (start_chan_proto_spec prot_loop); iIntros (c) "Hc".
-- 
GitLab