Commits · 9b4ce6dd4640f23adb8b019db9f6007f0e2ff878 · Gregory Malecha / stdpp

Mar 05, 2020
- Rename `fin_of_nat` → `nat_to_fin` to follow the conventions. · 9b4ce6dd
  Robbert Krebbers authored 5 years ago
  
  9b4ce6dd
- Function `fun_to_vec : (fin n → A) → vec A n`. · f0d2b68d
  Robbert Krebbers authored 5 years ago
  
  f0d2b68d
- Prove that `<` and `≤` are finite/infinite. · b668ba52
  Robbert Krebbers authored 5 years ago
  
  b668ba52
Feb 28, 2020
- Fix test in Coq 8.10 and 8.11. · 924d085e
  Robbert Krebbers authored 5 years ago
  
  924d085e
- declare Coq 8.9 and older as 'old' for reftests · 7c2aeaef
  Ralf Jung authored 5 years ago
  
  7c2aeaef
- Merge branch 'split_or' into 'master' · 85a5e4d7
  Robbert Krebbers authored 5 years ago
  
  Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption See merge request iris/stdpp!117
  85a5e4d7
- Changelog entry · 4f00de71
  Armaël Guéneau authored 5 years ago
  
  4f00de71
Feb 26, 2020
- Have destruct_and take care of [True] and destruct_or of [False] · 1e9a5ae9
  Armaël Guéneau authored 5 years ago
  
  The opposite was true before to this commit.
  1e9a5ae9
- Add destruct_or{?,!}, and generalize destruct_and{?,!} to handle an explicit assumption argument · 07c0cb06
  Armaël Guéneau authored 5 years ago
  
  07c0cb06
Feb 25, 2020
- Slight update to the documentation of [split_and{!,?}] · 03b166ab
  Armaël Guéneau authored 5 years ago
  
  03b166ab
Feb 24, 2020
- Merge branch 'robbert/vec_countable' into 'master' · 7d705c84
  Robbert Krebbers authored 5 years ago
  
  Countable instance for vec, and rename `vec_to_list_of_list` into `vec_to_list_to_vec` See merge request iris/stdpp!115
  7d705c84
- CHANGELOG entry. · 2d2a72ae
  Robbert Krebbers authored 5 years ago
  
  2d2a72ae
- Add `Countable` instance for `vec`. · 8b9dd4e5
  Robbert Krebbers authored 5 years ago
  
  8b9dd4e5
- Prove lemma `list_to_vec_to_list`. · 85f50214
  Robbert Krebbers authored 5 years ago
  
  85f50214
- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`. · 74e74b5a
  Robbert Krebbers authored 5 years ago
  
  74e74b5a
- Merge branch 'robbert/set_unfold_dom' into 'master' · 4fc67339
  Robbert Krebbers authored 5 years ago
  
  Add `set_solver` support for `dom` Closes #53 See merge request iris/stdpp!116
  4fc67339
- Add tests for `set_solver` on `dom`. · 5f26f6cd
  Robbert Krebbers authored 5 years ago
  
  5f26f6cd
- CHANGELOG entry. · 8e949e3c
  Robbert Krebbers authored 5 years ago
  
  8e949e3c
- Add `SetUnfold` instances for `dom`. · 78f50186
  Robbert Krebbers authored 5 years ago
  
  78f50186
- Put `LeibnizEquiv` lemmas for `dom` in section. · cb08e14f
  Robbert Krebbers authored 5 years ago
  
  cb08e14f
Feb 23, 2020
- Merge branch 'coGset' into 'master' · 268507ec
  Robbert Krebbers authored 5 years ago
  
  Rename `cogpick` to `coGpick` (oops). See merge request iris/stdpp!113
  268507ec
- Rename `cogpick` to `coGpick` (oops). · 248bc07a
  David Swasey authored 5 years ago
  
  248bc07a
Feb 20, 2020
- Merge branch 'cogset' into 'master' · 74649a4b
  Robbert Krebbers authored 5 years ago
  
  cogset See merge request iris/stdpp!108
  74649a4b
Feb 19, 2020
- Add `coGset`. · f5abe554
  David Swasey authored 5 years ago
  
  f5abe554
- Add lemma `not_elem_of_iff`. · 157ae750
  David Swasey authored 5 years ago
  
  157ae750
- Fix compilation after !112 broke it. · e0eef94a
  Robbert Krebbers authored 5 years ago
  
  e0eef94a
- Merge branch 'ralf/hints' into 'master' · f84c69f6
  Robbert Krebbers authored 5 years ago
  
  move coPset-generic hint to coPset.v See merge request iris/stdpp!112
  f84c69f6
- add comment · 829dc991
  Ralf Jung authored 5 years ago
  
  829dc991
- move coPset-generic hint to coPset.v · a5ee0c16
  Ralf Jung authored 5 years ago
  
  a5ee0c16
- Put `top_subseteq` in core DB to fix Iris regression. · 1f223f8f
  Robbert Krebbers authored 5 years ago
  
  1f223f8f
- test 8.11.dev instead of master · 06da8f18
  Ralf Jung authored 5 years ago
  
  06da8f18
Feb 18, 2020
- Merge branch 'robbert/top_set' into 'master' · af368a15
  Robbert Krebbers authored 5 years ago
  
  Add class `TopSet` for sets with ⊤ element Closes #49 See merge request !111
  af368a15
Feb 17, 2020
- CHANGELOG entry. · ab51e3fd
  Robbert Krebbers authored 5 years ago
  
  ab51e3fd
- `TopSet` instance for `boolset`. · 2ad56b99
  Robbert Krebbers authored 5 years ago
  
  2ad56b99
- Add class `TopSet` for sets with ⊤ element. · e09f7ce3
  Robbert Krebbers authored 5 years ago
  
  This closes issue #49.
  e09f7ce3
- Move lattice related stuff up. · ddfcc76c
  Robbert Krebbers authored 5 years ago
  
  ddfcc76c
- Remove obsolete `Hint Extern`s that predate the `Hint Mode` declarations. · 9a1b4cde
  Robbert Krebbers authored 5 years ago
  
  9a1b4cde
Feb 14, 2020
- `Prop` is inhabited. · 718ca5be
  Robbert Krebbers authored 5 years ago
  
  718ca5be
Feb 13, 2020
- Merge branch 'z-greater-decidability' into 'master' · b5a66ffb
  Robbert Krebbers authored 5 years ago
  
  Add decidability instances for Z.gt and Z.ge See merge request !110
  b5a66ffb
- Add decidability instances for Z.gt and Z.ge · 583c4645
  Tej Chajed authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  583c4645