From f52f9f6ab183f7d2bc94bd85a47db6ce18e006ef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Dec 2021 13:08:18 +0100
Subject: [PATCH] Bump std++.
---
coq-iris.opam | 2 +-
iris_heap_lang/proph_erasure.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/coq-iris.opam b/coq-iris.opam
index c6b6c48a0..9f5025d9c 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
depends: [
"coq" { (>= "8.12" & < "8.16~") | (= "dev") }
- "coq-stdpp" { (= "dev.2021-12-08.0.130789ac") | (= "dev") }
+ "coq-stdpp" { (= "dev.2021-12-09.0.e6194e28") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 8d96b7b00..dec086220 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -185,10 +185,10 @@ Proof.
split; [intros ?|intros (?&?&?)];
repeat (case_match; simplify_eq/=); eauto.
- eexists _; split; eauto; simpl.
- erewrite bool_decide_iff; first by eauto.
+ erewrite bool_decide_ext; first by eauto.
rewrite erase_val_inj_iff; done.
- by assert (vals_compare_safe v1 v2) by by apply vals_compare_safe_erase.
- - by erewrite bool_decide_iff; last apply erase_val_inj_iff.
+ - by erewrite bool_decide_ext; last apply erase_val_inj_iff.
- by assert (vals_compare_safe (erase_val v1) (erase_val v2))
by by apply vals_compare_safe_erase.
Qed.
--
GitLab