diff --git a/theories/lecture_notes/coq_intro_example_1.v b/theories/lecture_notes/coq_intro_example_1.v index cf2e23d68881df7c67fddc5aa52bc05450f72018..ccaebb202a96121ff46deee2eba750c41703858b 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 9fd6b0ac4077242ea77e63b3f08da1b2c580d9c6..2e56aa0a4e8badef8a6988543139d31ff341431e 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.