Commit 2dcc2a40 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris/coqstd++.

parent 1c1d4e0a
......@@ -5,8 +5,8 @@ This version is known to compile with:
- Coq 8.6.1
- Ssreflect 1.6
- Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- std++ version [fa6ff9d18aefb29e839e815aa170262d330bd108](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/fa6ff9d18aefb29e839e815aa170262d330bd108)
- Iris version [d85fdb0ea89edebcd10056e073ab9c7edc6c2050](https://gitlab.mpi-sws.org/FP/iris-coq/tree/d85fdb0ea89edebcd10056e073ab9c7edc6c2050)
- std++ version [24aef2fea9481e65d1f6658005ddde25ae9a64ee](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/24aef2fea9481e65d1f6658005ddde25ae9a64ee)
- Iris version [978965301130a145155e03e4858eef3f86f2c705](https://gitlab.mpi-sws.org/FP/iris-coq/tree/978965301130a145155e03e4858eef3f86f2c705)
# Compilation
......
......@@ -153,8 +153,8 @@ Proof.
by rewrite fmap_insert.
Qed.
Lemma delete_idem_binder {A} (x : binder) (m : stringmap A) :
Lemma delete_idemp_binder {A} (x : binder) (m : stringmap A) :
delete x (delete x m) = delete x m.
Proof.
destruct x; cbn; eauto. apply delete_idem.
destruct x; cbn; eauto. apply delete_idemp.
Qed.
......@@ -384,8 +384,8 @@ Proof.
by rewrite (delete_commute_binder _ f (BNamed x)).
+ apply not_and_l in H0 as [<-%dec_stable|<-%dec_stable].
* rewrite (delete_commute_binder _ x0 (BNamed x)).
by rewrite delete_idem_binder.
* by rewrite delete_idem_binder.
by rewrite delete_idemp_binder.
* by rewrite delete_idemp_binder.
Qed.
Lemma subst_p_rec (x1 x2 : binder) v1 v2 e :
......
Markdown is supported
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