Commits · swasey/sets-typeclass · Abel Nieto / Iris

Feb 25, 2020
- `namespace_map` notes. · 997bfe3f
  David Swasey authored 5 years ago
  
  997bfe3f
Feb 24, 2020
- `wsat` notes. · ecff9b3d
  David Swasey authored 5 years ago
  
  ecff9b3d
- Drop the canonical structures. · dedbd2c0
  David Swasey authored 5 years ago
  
  dedbd2c0
Feb 23, 2020
- WIP: Eliminate canonical structures in sets` to see what goes wrong. · fcbd0aa7
  David Swasey authored 5 years ago
  
  fcbd0aa7
- Adjust comment. · 5140c630
  David Swasey authored 5 years ago
  
  5140c630
- Try to clarify `fresh_setT`. · cb65a2e5
  David Swasey authored 5 years ago
  
  cb65a2e5
- Document why disjoint union doesn't work with . · 822007c2
  David Swasey authored 5 years ago
  
  822007c2
- Document suffixes used by `sets.v`. · f7094463
  David Swasey authored 5 years ago
  
  f7094463
- Avoid confusing "fresh elements". · 27a6563e
  David Swasey authored 5 years ago
  
  27a6563e
- Use canonical projections. · 7a7517c1
  David Swasey authored 5 years ago
  
  7a7517c1
- Improve packaging for set CMRAs. · aec35627
  David Swasey authored 5 years ago
  
  aec35627
- Typo in coqdoc. · f71d45e9
  David Swasey authored 5 years ago
  
  f71d45e9
- Document naming convention. · 14acb6a5
  David Swasey authored 5 years ago
  
  14acb6a5
- Typo. · 4bbb2d93
  David Swasey authored 5 years ago
  
  4bbb2d93
- Deprecate algebra/gset. · 33e32726
  David Swasey authored 5 years ago
  
  33e32726
- Deprecate algebra/coPset. · 57711e77
  David Swasey authored 5 years ago
  
  57711e77
- Add algebra/sets. · 72a643f0
  David Swasey authored 5 years ago
  
  72a643f0
Feb 21, 2020
- Bump stdpp. · 4974c4da
  David Swasey authored 5 years ago
  
  4974c4da
Feb 20, 2020
- Merge branch 'ralf/modalities' into 'master' · 4815e68e
  Ralf Jung authored 5 years ago
  
  say things about modalities See merge request iris/iris!377
  4815e68e
- say things about modalities · 8bc5a88a
  Ralf Jung authored 5 years ago
  
  8bc5a88a
Feb 19, 2020
- re-enable coqchk on coq master, for testing · 7ddea37a
  Ralf Jung authored 5 years ago
  
  7ddea37a
- Bump std++. · 96f40f26
  Robbert Krebbers authored 5 years ago
  
  96f40f26
- also build nightly against known-to-work Coq version · be509a69
  Ralf Jung authored 5 years ago
  
  be509a69
- CI: test Coq 8.11.dev on pushes, and master nightly · 8f75516d
  Ralf Jung authored 5 years ago
  
  8f75516d
- temporarily disable broken coqchk · beb9d445
  Ralf Jung authored 5 years ago
  
  beb9d445
Feb 18, 2020
- Merge branch 'robbert/intuitionistic_inv' into 'master' · 45383da9
  Ralf Jung authored 5 years ago
  
  Add introduction pattern `-# pat` to move a hypothesis to the spatial context Closes #213 See merge request iris/iris!370
  45383da9
- Remove more new lines. · 00bd9cf1
  Robbert Krebbers authored 5 years ago
  
  00bd9cf1
- And more useless new lines. · 461c88d6
  Robbert Krebbers authored 5 years ago
  
  461c88d6
- Remove useless newlines in `proof_mode.md`. · 1a5d7d58
  Robbert Krebbers authored 5 years ago
  
  1a5d7d58
- CHANGELOG entry for the `-# pat` intro pattern. · e9e00698
  Robbert Krebbers authored 5 years ago
  
  e9e00698
- Add tests for the `-# pat` intro pattern. · e53c2699
  Robbert Krebbers authored 5 years ago
  
  e53c2699
- Add proof mode documentation for the `-# pat` intro pattern. · 226b8579
  Robbert Krebbers authored 5 years ago
  
  226b8579
- Improve docs of the `# pat` intro pattern. · 25061957
  Robbert Krebbers authored 5 years ago
  
  25061957
- Add `-# pat` intro pattern to move a hypothesis to the spatial context. · c6a5d2d6
  Robbert Krebbers authored 5 years ago
  
  c6a5d2d6
- Stop using deprecated `!#` intro pattern. · 91cfdc1e
  Robbert Krebbers authored 5 years ago
  
  91cfdc1e
- Stop using deprecated `iAlways` tactic. · acd32497
  Robbert Krebbers authored 5 years ago
  
  acd32497
- Mark `iAlways` as deprecated in the code. · ad7eeccc
  Robbert Krebbers authored 5 years ago
  
  It was already marked as deprecated in `doc/proof_mode.md`.
  ad7eeccc
- Make names of constructors of `intro_pat` consistent with names of `tac_` lemmas. · 066b7f65
  Robbert Krebbers authored 5 years ago
  
  - Rename `IPureElim` -> `iPure`, `IAlwaysElim` -> `IIntuitionistic` - Drop `IAlwaysIntro` (it's just `IModalIntro`).
  066b7f65
- add another printing hint for normalization · 3b0457d4
  Ralf Jung authored 5 years ago
  
  3b0457d4
- note that 'Set Ltac Backtrace' is just a compat hack · f2e41316
  Ralf Jung authored 5 years ago
  
  f2e41316