- May 30, 2022
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 25, 2022
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 16, 2022
-
-
Ralf Jung authored
Enable cumulativity for telescopes Closes iris#461 See merge request iris/stdpp!380
-
Jan-Oliver Kaiser authored
-
Jan-Oliver Kaiser authored
The accessor test case also fails when the flag is enabled so that the dedicated test case for it never has a chance to run.
-
Jan-Oliver Kaiser authored
-
Ralf Jung authored
-
- May 13, 2022
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. See merge request iris/stdpp!378
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
make dom domain type paremeter (D) implicit Closes #137 See merge request iris/stdpp!376
-
Ralf Jung authored
- May 11, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
drop support for Coq 8.11 See merge request iris/stdpp!377
-
- May 09, 2022
-
-
Ralf Jung authored
-
- May 08, 2022
-
-
Ralf Jung authored
-
- May 06, 2022
- May 04, 2022
-
-
Ralf Jung authored
Annotate telescope notations to support literal telescope arguments. See merge request iris/stdpp!375
-
- May 03, 2022
-
-
Jan-Oliver Kaiser authored
-
Jan-Oliver Kaiser authored
-
- Apr 12, 2022
-
-
Robbert Krebbers authored
Add Pigeon Hole principle. See merge request iris/stdpp!373
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Add induction principle for `tele_arg`. See merge request iris/stdpp!374
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-