Commits · 21de4a0264e546035b4d4cda9c9bda05b44a7e39 · Iris / stdpp

May 28, 2021
- comply by opam's style guidelines · 21de4a02
  Ralf Jung authored 3 years ago
  
  21de4a02
- Merge branch 'robbert/countable_eq_dec' into 'master' · 3d845892
  Robbert Krebbers authored 3 years ago
  
  Comment about `EqDecision` in `Countable`. See merge request !268
  3d845892
- Comment about `EqDecision` in `Countable`. · aabff4ca
  Robbert Krebbers authored 3 years ago
  
  aabff4ca
- add explicit version name to opam package · da511623
  Ralf Jung authored 3 years ago
  
  da511623
May 27, 2021
- perform style checks in parallel with main build · e6fdf4fe
  Ralf Jung authored 3 years ago
  
  e6fdf4fe
- port a Makefile fix from Iris · 5a2cf2e2
  Ralf Jung authored 3 years ago
  
  5a2cf2e2
May 26, 2021
- changelog attribution consistency · 64ec9b56
  Ralf Jung authored 3 years ago
  
  64ec9b56
- Add `Inj` instances for `fmap` on option and maps. · 5424f22a
  Robbert Krebbers authored 3 years ago
  
  Thanks to @jules for pointing out these were missing.
  5424f22a
May 25, 2021
- More CHANGELOG. · 024bb001
  Robbert Krebbers authored 3 years ago
  
  024bb001
- Merge branch 'ralf/instances' into 'master' · 54d7f380
  Ralf Jung authored 3 years ago
  
  Explicit visibility for Instances See merge request !263
  54d7f380
- Local Instance → Definition · 89ebe23f
  Ralf Jung authored 3 years ago
  
  89ebe23f
- improve error message · eb035887
  Ralf Jung authored 3 years ago
  
  eb035887
- show line numbers in errors · 531fe4dd
  Ralf Jung authored 3 years ago
  
  531fe4dd
- also make sure Opaque/Transparent have visibility qualifiers · 56001965
  Ralf Jung authored 3 years ago
  
  56001965
- make local instances explicit · 6c010757
  Ralf Jung authored 3 years ago
  
  6c010757
- fix warnings about implicitly Global Instance · d0183a61
  Ralf Jung authored 3 years ago
  
  d0183a61
- Revert "Make `mapset_elem_of` Opaque." · cb1daa49
  Robbert Krebbers authored 3 years ago
  
  This reverts commit 267cc708. Thanks to @jung for spotting this was a NOP, see iris/stdpp!263 (comment 67379)
  cb1daa49
- Merge branch 'ralf/list-lookup' into 'master' · 13efa2cb
  Robbert Krebbers authored 3 years ago
  
  list lookup lemmas: cons, singleton See merge request iris/stdpp!264
  13efa2cb
- list lookup lemmas: cons, singleton · dc1d330a
  Ralf Jung authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  dc1d330a
May 20, 2021
- separate Coq 8.13 MR job from main job · 2948f2b8
  Ralf Jung authored 3 years ago
  
  2948f2b8
- set up CI for MRs · 2b5643ea
  Ralf Jung authored 3 years ago
  
  2b5643ea
- test name mangling on Coq 8.13 · 13a9cc66
  Ralf Jung authored 3 years ago
  
  13a9cc66
- remove ancient submodule leftovers · c3c2acbd
  Ralf Jung authored 3 years ago
  
  c3c2acbd
- Merge branch 'ralf/scope' into 'master' · 2060d37b
  Robbert Krebbers authored 3 years ago
  
  explicitly declare visibility of Scope actions See merge request iris/stdpp!262
  2060d37b
- explicitly declare visibility of Scope actions · 1681b494
  Ralf Jung authored 3 years ago
  
  1681b494
- add release date to changelog · d15f70a8
  Ralf Jung authored 3 years ago
  
  d15f70a8
- add credits to changelog · a06372a6
  Ralf Jung authored 3 years ago
  
  a06372a6
May 19, 2021
- Merge branch 'ralf/insert_take_drop' into 'master' · a01ba389
  Ralf Jung authored 3 years ago
  
  add insert_take_drop See merge request iris/stdpp!260
  a01ba389
- add insert_take_drop · 09111a57
  Ralf Jung authored 3 years ago
  
  09111a57
May 18, 2021
- Merge branch 'ralf/compute_done' into 'master' · 53f3a83d
  Robbert Krebbers authored 3 years ago
  
  add tactic for solving computable goals Closes #83 See merge request iris/stdpp!261
  53f3a83d
- coqdoc · c17ab51c
  Ralf Jung authored 3 years ago
  
  c17ab51c
May 17, 2021
- Merge branch 'msammler/little_endian' into 'master' · 814b1249
  Robbert Krebbers authored 3 years ago
  
  Add little endian encoding of Z See merge request iris/stdpp!254
  814b1249
- improve comment · cbc474cc
  Michael Sammler authored 3 years ago
  
  cbc474cc
May 13, 2021
- add compute_by · 14ccc4c8
  Ralf Jung authored 3 years ago
  
  14ccc4c8
May 11, 2021
- expand compute_done to handle a few more kinds of goals · c85d0f7a
  Ralf Jung authored 3 years ago
  
  c85d0f7a
May 07, 2021
- improve error on unqualified Hint · ae7bb15c
  Ralf Jung authored 3 years ago
  
  ae7bb15c
May 06, 2021
- Merge branch 'countable_sig' into 'master' · 02e61349
  Robbert Krebbers authored 3 years ago
  
  add Countable instance for decidable Sigma types See merge request iris/stdpp!255
  02e61349
May 05, 2021
- add Countable instance for decidable Sigma types · 1fb8aa47
  Simon Gregersen authored 3 years ago
  
  1fb8aa47
May 04, 2021
- rename conversion lemmas to follow convention · 2554d103
  Michael Sammler authored 3 years ago
  
  2554d103
- Use `Z.iter`. · dc5db80a
  Robbert Krebbers authored 3 years ago and Michael Sammler committed 3 years ago
  
  dc5db80a