Skip to content
Snippets Groups Projects
Commit f52f9f6a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump std++.

parent 0c23e92e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
coq-iris.opam
+ 1
− 1
View file @ f52f9f6a
...@@ -28,7 +28,7 @@ tags: [ ...@@ -28,7 +28,7 @@ tags: [
depends: [ depends: [
"coq" { (>= "8.12" & < "8.16~") | (= "dev") } "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}%"] build: ["./make-package" "iris" "-j%{jobs}%"]
......
iris_heap_lang/proph_erasure.v
+ 2
− 2
View file @ f52f9f6a
...@@ -185,10 +185,10 @@ Proof. ...@@ -185,10 +185,10 @@ Proof.
split; [intros ?|intros (?&?&?)]; split; [intros ?|intros (?&?&?)];
repeat (case_match; simplify_eq/=); eauto. repeat (case_match; simplify_eq/=); eauto.
- eexists _; split; eauto; simpl. - eexists _; split; eauto; simpl.
erewrite bool_decide_iff; first by eauto. erewrite bool_decide_ext; first by eauto.
rewrite erase_val_inj_iff; done. rewrite erase_val_inj_iff; done.
- by assert (vals_compare_safe v1 v2) by by apply vals_compare_safe_erase. - 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 assert (vals_compare_safe (erase_val v1) (erase_val v2))
by by apply vals_compare_safe_erase. by by apply vals_compare_safe_erase.
Qed. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment