Commits · 213cb42770c9881f6aa0607e82b9fe47b92309d2 · Iris / stdpp

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 !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 !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.
  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.
  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 !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 !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
- fix sed script · e32fc779
  Ralf Jung authored 4 years ago
  
  e32fc779
- Merge branch 'robbert/Qp' into 'master' · 402f2d6a
  Robbert Krebbers authored 4 years ago
  
  Extend the theory of positive rationals `Qp` See merge request !188
  402f2d6a
Oct 29, 2020
- Update sed script. · 420e57f6
  Robbert Krebbers authored 4 years ago
  
  420e57f6
- CHANGELOG. · e8adfd04
  Robbert Krebbers authored 4 years ago
  
  e8adfd04
- Tweaks based on feedback Ralf. · c7012583
  Robbert Krebbers authored 4 years ago
  
  c7012583
- Add lemmas for 1/4 + 1/4. · f106ebdd
  Robbert Krebbers authored 4 years ago
  
  f106ebdd
- Make `Qp` lemma names consistent with those for `Nat`, `Z` and friends. · b2f40d2a
  Robbert Krebbers authored 4 years ago
  
  b2f40d2a
- Rename `Qp_plus` → `Qp_add`, `Qp_mult` → `Qp_mul`, and `Qp_minus` → `Qp_sub`. · a30f6ade
  Robbert Krebbers authored 4 years ago
  
  a30f6ade
- Define `Qp` numerals in terms of `pos_to_Qp`. · da606ab1
  Robbert Krebbers authored 4 years ago
  
  da606ab1
- Add conversion function `pos_to_Qp` from `positive` to `Qp`. · b2903d4f
  Robbert Krebbers authored 4 years ago
  
  b2903d4f
- Define `Qp_inv`, and generalize `Qp_div` so both arguments range over `Qp`. · 2e4d59de
  Robbert Krebbers authored 4 years ago
  
  Moreover, and suitable lemmas.
  2e4d59de
- Use `let '(...) = ...` in definitions of `Qp_le` and `Qp_lt` to avoid eager unfolding. · 12590bc6
  Robbert Krebbers authored 4 years ago
  
  12590bc6
- Rename `Qp_eq` into `Qp_to_Qc_inj_iff`. · 9b68ea94
  Robbert Krebbers authored 4 years ago
  
  This follows the standard naming for Coq numbers, and avoids one using the old lemma to break abstraction accidentally.
  9b68ea94