| Age | Commit message (Expand) | Author |
|---|
| 2021-04-02 | add Cantor pairing to_nat and its inverse of_nat | Andrej Dudenhefner |
| 2021-03-26 | remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid | Andrej Dudenhefner |
| 2021-03-23 | add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map,... | Andrej Dudenhefner |
| 2021-03-23 | Merge PR #13671: [stdlib] [Vectors] add results on to_list | coqbot-app[bot] |
| 2021-03-23 | Merge PR #13804: [stdlib] [List] Add results about count_occ | coqbot-app[bot] |
| 2021-03-16 | correct changelog #13582 | Olivier Laurent |
| 2021-03-16 | add changelog | Olivier Laurent |
| 2021-02-26 | Signed primitive integers | Ana |
| 2021-02-25 | Merge PR #13080: Ascii: add leb and ltb | coqbot-app[bot] |
| 2021-01-29 | add changelog | Olivier Laurent |
| 2020-12-09 | Redefines exp_ineq1 to hold for all non-zero numbers. | Avi Shinnar |
| 2020-12-03 | Ascii: add leb and ltb | Yishuai Li |
| 2020-12-03 | [changelog] update markup | Enrico Tassi |
| 2020-12-03 | Changes for Coq 8.13 | Matthieu Sozeau |
| 2020-11-16 | Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-free | coqbot-app[bot] |
| 2020-11-13 | Add changelog for #13365 | Li-yao Xia |
| 2020-11-04 | [stdlib] Decidable instance for negation | Yishuai Li |
| 2020-09-07 | Add changelog entry | Edward Wang |
| 2020-08-25 | Require NsatzTactic: nsatz support for Z and Q | Jason Gross |
| 2020-08-24 | Put cyclic numbers in sort Set instead of Type | Vincent Semeria |
| 2020-08-13 | Merge PR #12799: [stdlib] [List] Additional statements about List.repeat | Anton Trunov |
| 2020-08-13 | Merge PR #12716: deprecate prod_curry and prod_uncurry | Anton Trunov |
| 2020-08-13 | Merge PR #12556: Bring Float notations in line with stdlib | Hugo Herbelin |
| 2020-08-12 | Additional statements about List.repeat | Olivier Laurent |
| 2020-08-11 | add deprecation to changelog | Yishuai Li |
| 2020-08-09 | Bring Int63 notations into line with stdlib | Jason Gross |
| 2020-08-09 | Bring Float notations in line with stdlib | Jason Gross |
| 2020-06-10 | Update changelog for 8.12+beta1. | Théo Zimmermann |
| 2020-06-09 | Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.leb | Guillaume Melquiond |
| 2020-06-09 | CReal: changed epsilon for modulus of convergence from 1/n to 2^z | Michael Soegtrop |
| 2020-06-08 | Fix 12483 | Pierre Roux |
| 2020-05-27 | Release notes for 8.12. | Théo Zimmermann |
| 2020-05-16 | Prove that classical reals implement constructive reals. Also move sums, min ... | Vincent Semeria |
| 2020-05-15 | Merge PR #11992: do not re-export ListNotations from Program | Anton Trunov |
| 2020-05-12 | Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.le | Anton Trunov |
| 2020-05-12 | fuse changelogs for #11249 and #12237 | Olivier Laurent |
| 2020-05-09 | Merge PR #12237: [stdlib] [List] add results around incl, filter and nth | Hugo Herbelin |
| 2020-05-09 | Merge PR #12263: HaskellExtr: Add type annotations to Prelude.== | Kazuhiko Sakaguchi |
| 2020-05-08 | Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpoints | Pierre-Marie Pédrot |
| 2020-05-07 | rename Bool.leb into Bool.le (same for ltb and compareb) | Olivier Laurent |
| 2020-05-06 | Merge PR #12008: [stdlib] Add order properties about bool | Anton Trunov |
| 2020-05-06 | HaskellExtr: Add type annotations to Prelude.== | Jason Gross |
| 2020-05-06 | Adding properties about implb. | Hugo Herbelin |
| 2020-05-04 | add order properties about bool | Olivier Laurent |
| 2020-05-04 | add incl_Forall_in_iff | Olivier Laurent |
| 2020-05-04 | add incl_map incl_filter NoDup_filter | Olivier Laurent |
| 2020-05-02 | Adding change logs for PR #12121. | Hugo Herbelin |
| 2020-04-30 | do not re-export ListNotations from Program: changelog | Antonio Nikishaev |
| 2020-04-24 | [nsatz] Use Export rather than Include | Jason Gross |
| 2020-04-24 | Split off Nsatz tactic part into NsatzTactic | Jason Gross |
