From 37145a3bc33e4400f5f2c10feba042a73a0c7ed2 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 19 Feb 2019 10:06:49 +0100 Subject: [PATCH] fix lecture_notes --- theories/lecture_notes/coq_intro_example_1.v | 2 +- theories/lecture_notes/modular_incr.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/lecture_notes/coq_intro_example_1.v b/theories/lecture_notes/coq_intro_example_1.v index cf2e23d..ccaebb2 100644 --- a/theories/lecture_notes/coq_intro_example_1.v +++ b/theories/lecture_notes/coq_intro_example_1.v @@ -140,7 +140,7 @@ Section proof. called wp_par. The two arguments are the conclusions of the two parallel threads. Here they are simply True, as in the paper proof when we used the ht-par rule. *) - iApply (wp_par (λ _ , ⌜True⌝)%I (λ _ , ⌜True⌝)%I). + wp_apply (wp_par (λ _ , ⌜True⌝)%I (λ _ , ⌜True⌝)%I). (* We now have three subgoals. The first two are proofs that each thread does the correct thing, and the final goal is to show that the combined conclusion of the two threads implies the desired conclusion. This last diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v index 9fd6b0a..2e56aa0 100644 --- a/theories/lecture_notes/modular_incr.v +++ b/theories/lecture_notes/modular_incr.v @@ -280,7 +280,7 @@ Section example_1. wp_let. wp_bind (_ ||| _)%E. let tac := iApply ("HIncr" with "[\$HInc]"); iNext; by iIntros (?) "_" in - iApply (wp_par (λ _, True%I) (λ _, True%I)); [tac | tac | ]. + wp_apply (wp_par (λ _, True%I) (λ _, True%I)); [tac | tac | ]. { iIntros (v1 v2) "_ !>". wp_seq. wp_apply (read_spec _ _ _ True%I (λ _, True%I)); auto. -- GitLab