Commits · coq-stdpp-1.2.1 · Lennard Gäher / stdpp

Aug 29, 2019
- release 1.2.1 · 75435486
  Ralf Jung authored 5 years ago
  
  View commits for tag coq-stdpp-1.2.1 coq-stdpp-1.2.1
  
  75435486
Aug 27, 2019
- Merge branch 'feature/binders' into 'master' · e3a5d03f
  Robbert Krebbers authored 5 years ago
  e3a5d03f
Aug 26, 2019
- Proofs about binders · 2883ab5a
  Michael Sammler authored 5 years ago
  
  2883ab5a
- Merge branch 'ralf/empty' into 'master' · aa051883
  Robbert Krebbers authored 5 years ago
  aa051883
- more instances for the empty type · af4cedfa
  Ralf Jung authored 5 years ago
  
  af4cedfa
- Merge branch 'ralf/empty' into 'master' · 1ae85171
  Robbert Krebbers authored 5 years ago
  1ae85171
- add Equiv instance for Empty_set · 12f82ad7
  Ralf Jung authored 5 years ago
  
  12f82ad7
Aug 24, 2019
- Credit @dfrumin in CHANGELOG. · adfc24d2
  Robbert Krebbers authored 5 years ago
  
  adfc24d2
- Merge branch 'map_zip_with_swap' into 'master' · 84708e6c
  Robbert Krebbers authored 5 years ago
  84708e6c
- Add `map_zip_with_flip`. · 273e12e9
  Dan Frumin authored 5 years ago
  
  273e12e9
Aug 23, 2019
- Remove useless space. · 62966bac
  Robbert Krebbers authored 5 years ago
  
  62966bac
- Merge branch 'nsteps_inv' into 'master' · 733ab29a
  Robbert Krebbers authored 5 years ago
  733ab29a
- relations.nsteps: add inversion lemma for `nsteps R 1 a b` · dfe225f7
  Paolo G. Giarrusso authored 5 years ago
  
  Verified
  
  dfe225f7
Aug 14, 2019
- Changelog tweaks, e.g. order contributes by first name. · 0b3d1e9f
  Robbert Krebbers authored 5 years ago
  
  0b3d1e9f
- Merge branch 'master' into 'master' · 48067dec
  Robbert Krebbers authored 5 years ago
  48067dec
- Add new lemmas for list, set, and map operations. · 6bc8803a
  Paulo Emílio de Vilhena authored 5 years ago
  
  6bc8803a
- Add `replicate_S_end`. · f9830af6
  Robbert Krebbers authored 5 years ago
  
  f9830af6
Aug 13, 2019
- Merge branch 'more_imap' into 'master' · 6827b242
  Robbert Krebbers authored 5 years ago
  6827b242
- More lemmas about [map_imap]. · f37ad033
  Rodolphe Lepigre authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  f37ad033
- Merge branch 'ralf/release-notes' into 'master' · d983fe55
  Robbert Krebbers authored 5 years ago
  d983fe55
Aug 07, 2019
- 1.2.1 release notes · 956644ce
  Ralf Jung authored 5 years ago
  
  956644ce
Jul 13, 2019
- Simplify proof of `list_find_ext`. · 3eb9d489
  Robbert Krebbers authored 5 years ago
  
  3eb9d489
- fix build for Coq 8.10 · 9eb8cd13
  Ralf Jung authored 5 years ago
  
  9eb8cd13
- Merge branch 'ralf/list-find-fmap' into 'master' · ec592463
  Robbert Krebbers authored 5 years ago
  ec592463
- use csimpl · 7748d9c5
  Ralf Jung authored 5 years ago
  
  7748d9c5
Jul 09, 2019
- more consistent lemma names · 09dc9e0d
  Ralf Jung authored 5 years ago
  
  09dc9e0d
Jul 08, 2019
- name fmap_inj · 2e0bf441
  Ralf Jung authored 5 years ago
  
  2e0bf441
Jul 07, 2019
- omap lemmas · 536c3662
  Ralf Jung authored 5 years ago
  
  536c3662
- fix list variable name · 1a019465
  Ralf Jung authored 5 years ago
  
  1a019465
- prove list_find_proper · 05bf88b7
  Ralf Jung authored 5 years ago
  
  05bf88b7
- prove list_find_fmap · 97ab0949
  Ralf Jung authored 5 years ago
  
  97ab0949
Jul 05, 2019
- Some results about `app` and `StronglySorted`. · 5f2a6b77
  Robbert Krebbers authored 5 years ago
  
  5f2a6b77
Jul 04, 2019
- Merge branch 'feature/imap_lemmas' into 'master' · 348cf509
  Robbert Krebbers authored 5 years ago
  348cf509
- Merge branch 'feature/list_lemmas' into 'master' · a4328503
  Robbert Krebbers authored 5 years ago
  a4328503
Jul 03, 2019
- some list related lemmas · 83746e0a
  Michael Sammler authored 5 years ago
  
  83746e0a
- some lemmas for seq and imap · 41fa0a31
  Michael Sammler authored 5 years ago
  
  41fa0a31
Jun 30, 2019
- Merge branch 'ralf/bool_decide' into 'master' · 02687b13
  Robbert Krebbers authored 5 years ago
  02687b13
- add invserses of bool_decide_{true,false} · 3db8e2f7
  Ralf Jung authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  3db8e2f7
- Fix bug in `solve_proper_prepare` to also handle unary functions. · 3b8eed3c
  Robbert Krebbers authored 5 years ago
  
  3b8eed3c
Jun 28, 2019
- Prove `set_Forall_list_to_set`. · ff0750f5
  Robbert Krebbers authored 5 years ago
  
  ff0750f5