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

Snippets Groups Projects

Mar 18, 2020
- Merge branch 'robbert/changelog' into 'master' · e61c2104
  Robbert Krebbers authored 5 years ago
  View commits for tag coq-stdpp-1.3.0 coq-stdpp-1.3.0
  
  e61c2104
Mar 17, 2020
- Compilation fixes. · ad2e80d6
  Robbert Krebbers authored 5 years ago
  ad2e80d6
- Update CHANGELOG for 1.3 release. · 731caa8a
  Robbert Krebbers authored 5 years ago
  
  731caa8a
- Merge branch 'robbert/seq_seqZ' into 'master' · f0bede87
  Robbert Krebbers authored 5 years ago
  f0bede87
- CHANGELOG. · 6b11b096
  Robbert Krebbers authored 5 years ago
  
  6b11b096
- Make lemmas for `seq` and `seqZ` consistent. · 2fa6c104
  Robbert Krebbers authored 5 years ago
  
  2fa6c104
- Fix Coqdoc. · b0033bce
  Robbert Krebbers authored 5 years ago
  
  b0033bce
- Merge branch 'robbert/lookup_total_lemmas' into 'master' · b04a1f11
  Robbert Krebbers authored 5 years ago
  b04a1f11
- More CHANGELOG. · 97079040
  Robbert Krebbers authored 5 years ago
  
  97079040
- CHANGELOG. · f05baf13
  Robbert Krebbers authored 5 years ago
  
  f05baf13
- Lemmas for `!!!` on lists. · 7ab0cff7
  Robbert Krebbers authored 5 years ago
  
  7ab0cff7
- Lemmas for `!!!` on `∅`, `delete`, `<[_:=_]>`, and `alter` operations on maps. · b3318a08
  Robbert Krebbers authored 5 years ago
  b3318a08
- Layout nits. · 368e2d77
  Robbert Krebbers authored 5 years ago
  
  368e2d77
Mar 13, 2020
- fix trailing empty line · 215f99da
  Ralf Jung authored 5 years ago
  
  215f99da
- license: remove unnecessary header with typo · a4d6b2a0
  Ralf Jung authored 5 years ago
  
  a4d6b2a0
- Merge branch 'robbert/copyright' into 'master' · 7e1f95ef
  Robbert Krebbers authored 5 years ago
  7e1f95ef
- Remove copyright headers, update LICENCE file. · 22a06f37
  Robbert Krebbers authored 5 years ago
  22a06f37
Mar 10, 2020
- Merge branch 'robbert/TCEq_hint' into 'master' · 8db97649
  Robbert Krebbers authored 5 years ago
  8db97649
- Change mode of `TCEq`. · e626f081
  Robbert Krebbers authored 5 years ago
  
  e626f081
- Merge branch 'robbert/TCX_hint_mode' into 'master' · 20ef8941
  Robbert Krebbers authored 5 years ago
  20ef8941
- Set `Hint Mode` for logical `TCX` type classes. · b130764f
  Robbert Krebbers authored 5 years ago
  
  b130764f
- Merge branch 'avoid-constr-hints' into 'master' · 3153d46d
  Robbert Krebbers authored 5 years ago
  3153d46d
- Avoid using Hint Resolve with a term · 7b5e32b9
  Tej Chajed authored 5 years ago
  7b5e32b9
Mar 09, 2020
- Tests for `set_unfold in H`. · f70ecc5c
  Robbert Krebbers authored 5 years ago
  
  f70ecc5c
- Add tactic `set_unfold in H`. · bd0e6352
  Robbert Krebbers authored 5 years ago
  
  bd0e6352
- Add lemma `fmap_map_seq`. · ddd73df1
  Robbert Krebbers authored 5 years ago
  
  ddd73df1
Mar 05, 2020
- Coq 8.10 compat. · b3e550a1
  Robbert Krebbers authored 5 years ago
  
  b3e550a1
- Merge branch 'robbert/nat_to_fin' into 'master' · a3d6c50e
  Robbert Krebbers authored 5 years ago
  a3d6c50e
- 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
  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
  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
  7d705c84
- CHANGELOG entry. · 2d2a72ae
  Robbert Krebbers authored 5 years ago
  
  2d2a72ae