Bump std++.

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-06-12.0.3cb65333") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-06-18.0.366d607e") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]

theories/logic/spec_rules.v

@@ -72,8 +72,8 @@ Section rules.
     iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ.
     rewrite to_tpool_insert'; last eauto.
     iFrame. iPureIntro.
-    apply rtc_nsteps in Hrtc; destruct Hrtc as [m Hrtc].
-    specialize (Hex HP). apply (nsteps_rtc (m + n)).
+    apply rtc_nsteps_1 in Hrtc; destruct Hrtc as [m Hrtc].
+    specialize (Hex HP). apply (rtc_nsteps_2 (m + n)).
     eapply nsteps_trans; eauto.
     revert e e' Htpj Hex.
     induction n => e e' Htpj Hex.

theories/typing/contextual_refinement_alt.v

@@ -78,7 +78,7 @@ Lemma rtc_erased_step_bot v tp1 tp2 σ1 σ2:
   rtc erased_step (bot #() :: tp1, σ1) (of_val v :: tp2, σ2) →
   False.
 Proof.
-  intros [n Hsteps]%rtc_nsteps. revert tp1 σ1 Hsteps.
+  intros [n Hsteps]%rtc_nsteps_1. revert tp1 σ1 Hsteps.
   induction (lt_wf n) as [n IH1 IH]=>tp1 σ1 Hsteps. destruct n as [|m].
   - inversion Hsteps.
   - inversion Hsteps; simplify_eq/=.