Commits · master · Paulo Emílio de Vilhena / stdpp · GitLab

Snippets Groups Projects

Feb 13, 2021
- CHANGELOG. · 8220d9a9
  Paulo Emílio de Vilhena authored 4 years ago
  
  8220d9a9
- Add context to section [map_filter_misc] and shorten some proofs. · 10636f91
  Paulo Emílio de Vilhena authored 4 years ago
  
  10636f91
Feb 12, 2021
- Remove [map_filter_lookup_eq]. · 388382c4
  Paulo Emílio de Vilhena authored 4 years ago
  
  388382c4
- CHANGELOG. · b68a10e9
  Paulo Emílio de Vilhena authored 4 years ago
  
  b68a10e9
- CHANGELOG.md · d8badd5e
  Paulo Emílio de Vilhena authored 4 years ago
  
  d8badd5e
- CHANGELOG. · b182e533
  Paulo Emílio de Vilhena authored 4 years ago
  
  b182e533
- Perform further amendments. · 1749dd30
  Paulo Emílio de Vilhena authored 4 years ago
  
  1749dd30
- Remove lemma [list_filter_alt]. · a1fc7de9
  Paulo Emílio de Vilhena authored 4 years ago
  
  a1fc7de9
- Add lemma about [list_to_set] composed with [elements]. · dbc36fe6
  Paulo Emílio de Vilhena authored 4 years ago
  
  dbc36fe6
- Apply proposed amendments to the MR. · 0f49e561
  Paulo Emílio de Vilhena authored 4 years ago
  
  0f49e561
- Add several simple lemmas (mostly about list and map filter). · 0608ef65
  Paulo Emílio de Vilhena authored 4 years ago
  
  0608ef65
- Add some type annotations. · d3feb6b5
  Robbert Krebbers authored 4 years ago
  
  d3feb6b5
- Merge branch 'simpl-never-fix' into 'master' · 92e7ad56
  Robbert Krebbers authored 4 years ago
  92e7ad56
Feb 11, 2021
- Avoid relying on buggy simpl never behavior · bfca791e
  Tej Chajed authored 4 years ago
  bfca791e
Feb 09, 2021
- Merge branch 'ralf/nat-iter-mul' into 'master' · 7309dfa2
  Robbert Krebbers authored 4 years ago
  7309dfa2
- add Nat_iter_mul · 70a21632
  Ralf Jung authored 4 years ago
  
  70a21632
Feb 01, 2021
- Merge branch 'ralf/pred_infinite_surj' into 'master' · bcebd707
  Ralf Jung authored 4 years ago
  bcebd707
- Merge branch 'ralf/gset_eq' into 'master' · 58c0e8cb
  Ralf Jung authored 4 years ago
  58c0e8cb
- rename elem_of_equiv -> set_equiv and set_equiv_spec -> set_equiv_subseteq,... · 46cc81ad
  Ralf Jung authored 4 years ago
  46cc81ad
Jan 29, 2021
- Do not mangle names in test file. · c7f299a5
  Robbert Krebbers authored 4 years ago
  
  c7f299a5
- generalize to two different types · 5728445c
  Ralf Jung authored 4 years ago
  
  5728445c
- Merge branch 'robbert/eunify' into 'master' · e377efdf
  Robbert Krebbers authored 4 years ago
  e377efdf
- CHANGELOG. · eca37705
  Robbert Krebbers authored 4 years ago
  
  eca37705
- Test cases for `eunify`. · f6a91817
  Robbert Krebbers authored 4 years ago
  
  f6a91817
- Add `eunify` tactic. · ddfd5b06
  Robbert Krebbers authored 4 years ago
  
  ddfd5b06
- add pred_infinite_surj · 996a098d
  Ralf Jung authored 4 years ago
  
  996a098d
Jan 28, 2021
- Do not declare tests as Instances. · c63e3678
  Robbert Krebbers authored 4 years ago
  
  c63e3678
- Merge branch 'robbert/Forall_Forall2_diag' into 'master' · 889d99ae
  Ralf Jung authored 4 years ago
  889d99ae
- Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the · 1bce0e36
  Robbert Krebbers authored 4 years ago
  1bce0e36
- Merge branch 'robbert/1_1_1_2' into 'master' · b9014191
  Robbert Krebbers authored 4 years ago
  b9014191
Jan 27, 2021
- tests/tactics: do not depend on variable name · 1a2061bd
  Ralf Jung authored 4 years ago
  
  1a2061bd
- Merge branch 'robbert/select_last' into 'master' · e97b9309
  Ralf Jung authored 4 years ago
  e97b9309
- Expand comment in `select`; based on `iSelect` in Iris. · cf9f43cb
  Robbert Krebbers authored 4 years ago
  
  cf9f43cb
- Fix documentation of `select` to state that it selects the "last" hypothesis. · 06531b45
  Robbert Krebbers authored 4 years ago
  
  06531b45
- Rename `_11` and `_12` suffixes into `_1_1` and `_1_2`. · 1ffab116
  Robbert Krebbers authored 4 years ago
  
  1ffab116
Jan 23, 2021
- Merge branch 'robbert/omap' into 'master' · 1f7d13f3
  Ralf Jung authored 4 years ago
  1f7d13f3
- Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}` · 0b4f16bf
  Robbert Krebbers authored 4 years ago and Ralf Jung committed 4 years ago
  0b4f16bf
Jan 20, 2021
- Fix compilation with Coq 8.10 and 8.11. · e386a738
  Robbert Krebbers authored 4 years ago
  
  e386a738
- Merge branch 'robbert/map_lookup_total' into 'master' · 9f3e4929
  Robbert Krebbers authored 4 years ago
  9f3e4929
- Merge branch 'ralf/map_zip_diag' into 'master' · 2bc4c093
  Robbert Krebbers authored 4 years ago
  2bc4c093