- 16 Dec, 2021 4 commits
-
-
Robbert Krebbers authored
Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`. See merge request !352
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 13 Dec, 2021 2 commits
-
-
Robbert Krebbers authored
remove a Global Arguments Pos.of_nat from the middle of a proof See merge request !350
-
Ralf Jung authored
-
- 09 Dec, 2021 1 commit
-
-
Robbert Krebbers authored
Homomorphism properties for `bool_decide` + rename (bool_)decide_iff. See merge request iris/stdpp!348
-
- 08 Dec, 2021 3 commits
-
-
Ralf Jung authored
Fix list_fmap_inj_1 See merge request iris/stdpp!349
-
Michael Sammler authored
-
Ralf Jung authored
-
- 07 Dec, 2021 7 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
add bool_decide_negb See merge request !347
-
Robbert Krebbers authored
Add is_closed_term tactic See merge request !345
-
Michael Sammler authored
-
Robbert Krebbers authored
Avoid using Arith libraries deprecated in v8.16 See merge request !346
-
- 06 Dec, 2021 6 commits
-
-
Ralf Jung authored
-
-
Robbert Krebbers authored
Add list_fmap_inj1, Z_to_little_endian_lookup_Some and little_endian_to_Z_spec See merge request !344
-
Ralf Jung authored
-
Tej Chajed authored
-
Tej Chajed authored
-
- 04 Dec, 2021 1 commit
-
-
Ralf Jung authored
-
- 03 Dec, 2021 7 commits
-
-
Michael Sammler authored
-
-
Michael Sammler authored
-
Ralf Jung authored
drop support for Coq 8.10 See merge request iris/stdpp!342
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- 02 Dec, 2021 1 commit
-
-
Robbert Krebbers authored
`zip_with_take_{l,r,both}{,'}` (was: Add lemma `zip_with_take_both`) See merge request iris/stdpp!339
-
- 01 Dec, 2021 8 commits
-
-
Ralf Jung authored
some more lemmas about list folding See merge request iris/stdpp!343
-
-
Glen Mével authored
-
Glen Mével authored
-
Glen Mével authored
-
Michael Sammler authored
-
Michael Sammler authored
Add bool_to_Z See merge request iris/stdpp!341
-
Michael Sammler authored
-
