Forked from
Iris / Iris
5354 commits behind the upstream repository.
-
Robbert Krebbers authored
It now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.
Robbert Krebbers authoredIt now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.
opam.pins 104 B
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 3103b7bf52d0275f2938d9af44ab2d0db89a6251