Commits · coq-stdpp-1.2.0 · Lennard Gäher / stdpp · GitLab

Snippets Groups Projects

Apr 26, 2019
- release version 1.2.0 · 10bc4e2a
  Ralf Jung authored 6 years ago
  
  View commits for tag coq-stdpp-1.2.0 coq-stdpp-1.2.0
  
  10bc4e2a
- Rename `NoBackTrack` into `TCNoBackTrack`. · 32eab16e
  Robbert Krebbers authored 6 years ago
  
  32eab16e
- Update CHANGELOG.md · b52e911c
  Ralf Jung authored 6 years ago
  
  b52e911c
- CHANGELOG. · 65f8c130
  Robbert Krebbers authored 6 years ago
  
  65f8c130
Apr 25, 2019
- More type annotations for https://github.com/coq/coq/pull/9996 . · d6eb24f2
  Robbert Krebbers authored 6 years ago
  
  d6eb24f2
- Merge branch 'robbert/binders' into 'master' · 0f2d2c8a
  Robbert Krebbers authored 6 years ago
  0f2d2c8a
- Binders library that's used in many Iris developments. · 9054147a
  Robbert Krebbers authored 6 years ago
  
  9054147a
Apr 24, 2019
- Generalize `gset_to_propset` to `set_to_propset` for any SemiSet. · 809e0d1d
  Robbert Krebbers authored 6 years ago
  809e0d1d
- Merge branch 'ci/robbert/setunfold' into 'master' · ff302761
  Ralf Jung authored 6 years ago
  ff302761
- New class `SetUnfoldElemOf` that specializes `SetUnfold` to improve performance. · f6b1bf4b
  Robbert Krebbers authored 6 years ago
  
  f6b1bf4b
Apr 19, 2019
- Merge branch 'gmultiset_lemmas' into 'master' · a8e9b673
  Robbert Krebbers authored 6 years ago
  a8e9b673
- gmultiset lemmas · 812f01bf
  Dan Frumin authored 6 years ago and Robbert Krebbers committed 6 years ago
  
  812f01bf
Mar 26, 2019
- Merge branch 'map_zip_with' into 'master' · d98ab4e4
  Robbert Krebbers authored 6 years ago
  d98ab4e4
- Remove a trailing whitespace · 0fe5f842
  Dan Frumin authored 6 years ago
  
  0fe5f842
- Add `map_delete_zip_with`. · af40bc7b
  Dan Frumin authored 6 years ago
  
  af40bc7b
Mar 16, 2019
- Fix some Coqdoc, e.g. use `[ ]` for code, that I did not see in the review of !62, · 700545bb
  Robbert Krebbers authored 6 years ago
  
  700545bb
- Merge branch 'better-list-countable' into 'master' · 3666e81e
  Robbert Krebbers authored 6 years ago
  3666e81e
- More efficient list encoding for Countable · 9b209c98
  Jakob Botsch Nielsen authored 6 years ago and Robbert Krebbers committed 6 years ago
  9b209c98
Mar 15, 2019
- Fix weird thing that should not have worked. · 03127e9d
  Robbert Krebbers authored 6 years ago
  
  03127e9d
- tweak COQTEST output · 862c6904
  Ralf Jung authored 6 years ago
  
  862c6904
- make NO_TEST=1 skips the tests · b1d043ef
  Ralf Jung authored 6 years ago
  
  b1d043ef
- Make `mapset_elem_of` Opaque. · 267cc708
  Robbert Krebbers authored 6 years ago
  267cc708
- Put list notations like `(++)` in `list_scope` instead of `stdpp_scope`. · 48bded44
  Robbert Krebbers authored 6 years ago
  
  48bded44
Mar 14, 2019
- remove a stale comment · f9480244
  Ralf Jung authored 6 years ago
  
  f9480244
- Merge branch 'ralf/readme' into 'master' · bf6816e3
  Robbert Krebbers authored 6 years ago
  bf6816e3
- move the (very brief) contribution guide to the README · bfa89673
  Ralf Jung authored 6 years ago
  
  bfa89673
- Merge branch 'robbert/gset_definition' into 'master' · e2eb2948
  Robbert Krebbers authored 6 years ago
  e2eb2948
- Make `gset` a `Definition` instead of `Notation`. · dfec102c
  Robbert Krebbers authored 6 years ago
  
  dfec102c
- Make `mapset_countable` a global instance. · d0961b67
  Robbert Krebbers authored 6 years ago
  
  d0961b67
Mar 06, 2019
- Removed unused argument for `map_seq` lemmas. · 22e0ade7
  Robbert Krebbers authored 6 years ago
  
  22e0ade7
Mar 04, 2019
- Make `fresh` stuff `simpl never`. · b938e033
  Robbert Krebbers authored 6 years ago
  b938e033
Mar 03, 2019
- Merge branch 'robbert/infinite' into 'master' · 7b80dd85
  Robbert Krebbers authored 6 years ago
  7b80dd85
- Prove `pred_infinite (λ _: A, True)` for `A` infinite. · c04c1337
  Robbert Krebbers authored 6 years ago
  
  c04c1337
- Overhaul of the `Infinite`/`Fresh` infrastructure. · 3184ef61
  Robbert Krebbers authored 6 years ago
  3184ef61
Mar 01, 2019
- Ensure that `Nat.max` only `simpl`s if it does not result into a pattern match. · 0a0bd5d2
  Robbert Krebbers authored 6 years ago
  
  0a0bd5d2
- Permutation Proper instance for `omap` on lists. · fa8a02f2
  Robbert Krebbers authored 6 years ago
  
  fa8a02f2
- More properties about filter on lists. · 56fe186d
  Robbert Krebbers authored 6 years ago
  
  56fe186d
- Monotonicity for `Acc`. · 1d45f474
  Robbert Krebbers authored 6 years ago
  
  1d45f474
Feb 28, 2019
- auto-detect timing project name even more · 7b4dc84f
  Ralf Jung authored 6 years ago
  
  7b4dc84f
- auto-detect timing project name · f7396465
  Ralf Jung authored 6 years ago
  
  f7396465