Commits · coq-stdpp-1.0 · Simon Friis Vindum / stdpp · GitLab

Snippets Groups Projects

Feb 14, 2017
- opam: fix uninstall · b8ffa59a
  Ralf Jung authored 8 years ago
  
  b8ffa59a
- add homepage to opam file · af37201f
  Ralf Jung authored 8 years ago
  
  af37201f
Feb 13, 2017
- edit opam file · 92bb54a9
  Ralf Jung authored 8 years ago
  
  View commits for tag coq-stdpp-1.0.0 coq-stdpp-1.0.0
  
  92bb54a9
- Add a contributor's guide · 2ac607ba
  Robbert Krebbers authored 8 years ago
  2ac607ba
Feb 10, 2017
- Make arguments for sig and sigT constructors and projections maximally implicit. · 613168bf
  Robbert Krebbers authored 8 years ago
  613168bf
Feb 09, 2017
- Prove elem_of_submseteq. · c1687739
  Robbert Krebbers authored 8 years ago
  
  c1687739
- Propers for monadic operations on option. · 0144c537
  Robbert Krebbers authored 8 years ago
  
  0144c537
Feb 07, 2017
- Merge branch 'ralf/buildsys' into 'master' · aad23129
  Robbert Krebbers authored 8 years ago
  aad23129
- update build system, CI and README · 2d8a4eb4
  Ralf Jung authored 8 years ago
  
  2d8a4eb4
- Also support Coq 8.5pl3. · 10c2f692
  Robbert Krebbers authored 8 years ago
  
  10c2f692
- Fix typo. · e1762d72
  Robbert Krebbers authored 8 years ago
  
  e1762d72
Feb 06, 2017
- Move COQ FLAGS to _CoqProject. · 5052a548
  Robbert Krebbers authored 8 years ago
  
  5052a548
Feb 03, 2017
- Make f_equiv stronger. · 2c261344
  Robbert Krebbers authored 8 years ago
  2c261344
- add opam and CI stuff (with preliminary names) · 63f64743
  Ralf Jung authored 8 years ago
  
  63f64743
- Add README. · c82f6e43
  Robbert Krebbers authored 8 years ago
  
  c82f6e43
- Add makefiles and license. · 1ef65e1b
  Robbert Krebbers authored 8 years ago
  
  1ef65e1b
Jan 31, 2017
- A bunch of missing Params instances. · 4b0631bb
  Robbert Krebbers authored 8 years ago
  
  4b0631bb
- Operations for converting between maps and collections. · e54b7fe0
  Robbert Krebbers authored 8 years ago
  e54b7fe0
- Curry and uncurry operations on gmap. · 7cd44ad5
  Robbert Krebbers authored 8 years ago
  
  7cd44ad5
- Fold operation on finite maps. · c134e48c
  Robbert Krebbers authored 8 years ago
  
  c134e48c
- Bump year in prelude copyright headers. · a89c6d78
  Robbert Krebbers authored 8 years ago
  
  a89c6d78
- Vector tweaks. · 845e9b73
  Robbert Krebbers authored 8 years ago
  
  845e9b73
- Use primitive projections for sealing · eebf68aa
  Ralf Jung authored 8 years ago
  eebf68aa
- Make instances EqDecision and Countable of gmultiset less eager. · 2e2351cd
  Robbert Krebbers authored 8 years ago
  2e2351cd
- Recursive [inv_vec]. · 3ebeaca2
  Jacques-Henri Jourdan authored 8 years ago
  
  3ebeaca2
- Renaming in prelude/list. · 0158faa7
  Robbert Krebbers authored 8 years ago
  0158faa7
- more restrictive Proof Using hints in (most files of the) prelude · 808b681c
  Ralf Jung authored 8 years ago
  
  808b681c
- Tweak some proof using tweaks for setoid stuff. · 24623c52
  Robbert Krebbers authored 8 years ago
  
  24623c52
- tune "Proof using" directives to minimize differences to previous types of all lemmas · 47e0f1c4
  Ralf Jung authored 8 years ago
  
  47e0f1c4
- don't use Proof Using in a few files that get too many unnecessary annotations from this · ee3e02f0
  Ralf Jung authored 8 years ago
  
  ee3e02f0
- Require `Total R` just for the merge sort theorems that actually need it. · 2028fae1
  Robbert Krebbers authored 8 years ago
  
  2028fae1
- Document list_remove and list_remove_list. · 649f7c76
  Robbert Krebbers authored 8 years ago
  
  649f7c76
- Fix more _L lemmas. · 4fd8d550
  Robbert Krebbers authored 8 years ago
  
  4fd8d550
- make "make quick" quick by adding hints about the used section variables · 108d1f8d
  Ralf Jung authored 8 years ago
  108d1f8d
- add decide_left, decide_right · 50b9555d
  Ralf Jung authored 8 years ago
  
  50b9555d
- Move stuff out of sections that does not depend on the section variables. · cab3033b
  Robbert Krebbers authored 8 years ago
  
  cab3033b
- Simplify proofs relating nth to lookup. · b084730a
  Robbert Krebbers authored 8 years ago
  b084730a
- list: relate nth and lookup · cdcfeee8
  Ralf Jung authored 8 years ago
  
  cdcfeee8
- A few lemmas about vec and fin. · 30b2cbc7
  Jacques-Henri Jourdan authored 8 years ago
  
  30b2cbc7
Dec 09, 2016
- Rename fmap_Some_equiv' → fmap_Some_equiv_1. · d631fdde
  Robbert Krebbers authored 8 years ago
  d631fdde