Commits · 77e40221afe24e6fb2fae2a0831702fe6dc71c57 · Thibaut Pérami / stdpp

Jan 11, 2021
- Merge branch 'ralf/take_0' into 'master' · 77e40221
  Robbert Krebbers authored 4 years ago
  
  prove take_0 See merge request iris/stdpp!209
  77e40221
- prove take_0 · 3c4993d2
  Ralf Jung authored 4 years ago
  
  3c4993d2
Jan 08, 2021
- make sure all Instance/Argument/Hint are qualified · 3ae73218
  Ralf Jung authored 4 years ago
  
  3ae73218
Jan 07, 2021
- Merge branch 'ralf/explicit-local-global' into 'master' · 43aea848
  Robbert Krebbers authored 4 years ago
  
  explicit Local/Global for all Instance, Arguments, Hint See merge request !207
  43aea848
- also adjust Hint · 3081c441
  Ralf Jung authored 4 years ago
  
  3081c441
- explicit Local/Global for all Instance and Arguments · 8709344e
  Ralf Jung authored 4 years ago
  
  8709344e
- Merge branch 'robbert/fmap_empty' into 'master' · df64edb2
  Robbert Krebbers authored 4 years ago
  
  Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename... See merge request iris/stdpp!205
  df64edb2
Jan 04, 2021
- Indent nested sections in `fin_maps` file. · 794f33f6
  Robbert Krebbers authored 4 years ago
  
  794f33f6
- Add lemma `bind_Some_equiv`. · abe0ec66
  Robbert Krebbers authored 4 years ago
  
  abe0ec66
- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename... · 46b16f58
  Robbert Krebbers authored 4 years ago
  
  Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
  46b16f58
Dec 24, 2020
- Add `pretty` instance for `positive`. · 7bf7c7fa
  Robbert Krebbers authored 4 years ago
  
  7bf7c7fa
Dec 11, 2020
- fix build on macOS · 881f2f38
  Ralf Jung authored 4 years ago
  
  881f2f38
Dec 10, 2020
- update test harness · e41e169f
  Ralf Jung authored 4 years ago
  
  e41e169f
Dec 09, 2020
- also accept installing with Coq 8.13 beta · 213cb427
  Ralf Jung authored 4 years ago
  
  213cb427
Dec 04, 2020
- Merge branch 'ralf/insert_subseteq_l' into 'master' · 0b4f0dd1
  Robbert Krebbers authored 4 years ago
  
  add insert_subseteq_l See merge request iris/stdpp!204
  0b4f0dd1
- better proof by Robbert · 4a5f19ed
  Ralf Jung authored 4 years ago
  
  4a5f19ed
- add insert_subseteq_l · 5acbf503
  Ralf Jung authored 4 years ago
  
  5acbf503
Nov 26, 2020
- bump CI to Coq 8.12.1 · fd7f5e42
  Ralf Jung authored 4 years ago
  
  fd7f5e42
- Merge branch 'fix-unused-variable-warnings' into 'master' · 41b8ca41
  Robbert Krebbers authored 4 years ago
  
  Replace unused pattern variables with underscore See merge request iris/stdpp!203
  41b8ca41
Nov 23, 2020
- Replace unused pattern variables with underscore · b920e707
  Tej Chajed authored 4 years ago
  
  Addresses new unused-pattern-matching-variable warning on Coq master.
  Verified
  
  b920e707
- Merge branch 'fix-hint-locality' into 'master' · 94d45b1c
  Robbert Krebbers authored 4 years ago
  
  Add explicit Global to hints at top level See merge request iris/stdpp!202
  94d45b1c
Nov 20, 2020
- Add explicit Global to hints at top level · 8e8f3a41
  Tej Chajed authored 4 years ago
  
  Fixes new Coq master warning deprecated-hint-without-locality.
  Verified
  
  8e8f3a41
Nov 15, 2020
- re-enable name mangling check · e88411b5
  Ralf Jung authored 4 years ago
  
  e88411b5
Nov 12, 2020
- Merge branch 'robbert/pretty_hint_mode' into 'master' · fb289f0b
  Robbert Krebbers authored 4 years ago
  
  Set `Hint Mode` for `pretty`. See merge request iris/stdpp!201
  fb289f0b
- CHANGELOG. · 846cb082
  Robbert Krebbers authored 4 years ago
  
  846cb082
- Set `Hint Mode` for `pretty`. · 00e2ceeb
  Robbert Krebbers authored 4 years ago
  
  00e2ceeb
Nov 11, 2020
- update Makefile · 6385b547
  Ralf Jung authored 4 years ago
  
  6385b547
- disable name mangling while Coq is broken · 15a5a4ef
  Ralf Jung authored 4 years ago
  
  15a5a4ef
- update CI config · 33492bdf
  Ralf Jung authored 4 years ago
  
  33492bdf
Nov 10, 2020
- Merge branch 'add-lemma' into 'master' · dcfe9839
  Robbert Krebbers authored 4 years ago
  
  Add lemmas about `list_to_map` See merge request iris/stdpp!199
  dcfe9839
- Merge branch 'robbert/pretty_0' into 'master' · 92b285f8
  Robbert Krebbers authored 4 years ago
  
  Pretty-print 0 as "0" for N, Z, and nat See merge request iris/stdpp!200
  92b285f8
- Refactor proof of list_to_map_snoc · 4f541628
  Simon Friis Vindum authored 4 years ago
  
  4f541628
- CHANGELOG. · a73ac825
  Robbert Krebbers authored 4 years ago
  
  This is a copy/paste of the CHANGELOG in iris/stdpp!198.
  a73ac825
- Test cases for `pretty` of `N`, `nat`, and `Z`. · 2b610e92
  Robbert Krebbers authored 4 years ago
  
  2b610e92
- Fix `pretty` for `Z` and prove `injectivity` of it. · 359bdf0f
  Robbert Krebbers authored 4 years ago
  
  359bdf0f
- Fix `pretty` for `N`. · 1855e425
  Robbert Krebbers authored 4 years ago
  
  This fix is inspired by iris/stdpp!198.
  1855e425
Nov 09, 2020
- Add lemmas about list_to_map · 1b9b1ef7
  Simon Friis Vindum authored 4 years ago
  
  1b9b1ef7
Nov 02, 2020
- update Makefile · 1b559061
  Ralf Jung authored 4 years ago
  
  1b559061
Oct 31, 2020
- Update CHANGELOG for Qp changes. · d0f75495
  Robbert Krebbers authored 4 years ago
  
  d0f75495
Oct 30, 2020
- move Qp changelogs entries together, and remove outdated ones · 98cf371f
  Ralf Jung authored 4 years ago
  
  98cf371f