From 9152955df0f066cf68dfe5d95eddbe343ef4701f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Jun 2021 08:57:59 +0200
Subject: [PATCH] Bump std++.
---
opam | 2 +-
theories/logic/spec_rules.v | 4 ++--
theories/typing/contextual_refinement_alt.v | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/opam b/opam
index 760461c..aa2413c 100644
--- a/opam
+++ b/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" }
]
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index cf519ed..7cc744d 100644
--- a/theories/logic/spec_rules.v
+++ b/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.
diff --git a/theories/typing/contextual_refinement_alt.v b/theories/typing/contextual_refinement_alt.v
index c83d344..e52c6a4 100644
--- a/theories/typing/contextual_refinement_alt.v
+++ b/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/=.
--
GitLab