| Age | Commit message (Expand) | Author |
|---|
| 2021-04-17 | Properly pass the Ltac2 notation level to the gramlib API. | Pierre-Marie Pédrot |
| 2021-04-16 | Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation. | coqbot-app[bot] |
| 2021-04-13 | Merge PR #14024: [coqdep] error on non-existent and unreadable files | coqbot-app[bot] |
| 2021-04-12 | [coqdep] error on non-existent and unreadable files | Hendrik Tews |
| 2021-04-12 | Merge PR #14107: Gitignore update for doc_grammar and omega clean-up. | coqbot-app[bot] |
| 2021-04-12 | Remove omega from doc_grammar files. | Théo Zimmermann |
| 2021-04-10 | Merge PR #14091: Fix link in doc/cic.rst, there is no Credits chapter anymore | coqbot-app[bot] |
| 2021-04-10 | Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on red/or... | coqbot-app[bot] |
| 2021-04-10 | Fix link in doc/cic.rst, there is no Credits chapter anymore | Yannick Forster |
| 2021-04-08 | Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular. | Pierre-Marie Pédrot |
| 2021-04-07 | Merge PR #14008: [stdlib] [Arith] Cantor pairing | coqbot-app[bot] |
| 2021-04-06 | Merge PR #14077: Add odoc warnings for empty packages. | coqbot-app[bot] |
| 2021-04-06 | Merge PR #13741: Remove omega tactic (deprecated in 8.12) | coqbot-app[bot] |
| 2021-04-06 | Add odoc warnings for empty packages. | Théo Zimmermann |
| 2021-04-04 | Adding change log for #13624. | Hugo Herbelin |
| 2021-04-02 | Remove the omega tactic and related options | Jim Fehrle |
| 2021-04-02 | add Cantor pairing to_nat and its inverse of_nat | Andrej Dudenhefner |
| 2021-04-01 | Merge PR #14044: [RM] changelog for 8.13.2 | coqbot-app[bot] |
| 2021-04-01 | Merge PR #14018: [doc] [coq_makefile] Document that -j N is broken for OCaml ... | coqbot-app[bot] |
| 2021-04-01 | Update doc/sphinx/changes.rst | Enrico Tassi |
| 2021-04-01 | Update doc/sphinx/changes.rst | Enrico Tassi |
| 2021-04-01 | changelog for 8.13.2 | Enrico Tassi |
| 2021-03-30 | Properly expand projection parameters in Btermdn. | Pierre-Marie Pédrot |
| 2021-03-30 | Merge PR #14012: Fix Ltac2 `Array.init` exponential overhead | Pierre-Marie Pédrot |
| 2021-03-30 | Merge PR #14005: Support OCaml primitives with an actual arity larger than 4. | Pierre-Marie Pédrot |
| 2021-03-30 | Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers. | Michael Soegtrop |
| 2021-03-29 | [doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0 | Emilio Jesus Gallego Arias |
| 2021-03-29 | Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies:... | coqbot-app[bot] |
| 2021-03-29 | Added a changelog. | Pierre-Marie Pédrot |
| 2021-03-26 | Document as critical. | Guillaume Melquiond |
| 2021-03-26 | Fix Ltac2 `Array.init` exponential overhead | Jason Gross |
| 2021-03-26 | Adding a changelog. | Pierre-Marie Pédrot |
| 2021-03-26 | remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid | Andrej Dudenhefner |
| 2021-03-26 | Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmas | coqbot-app[bot] |
| 2021-03-25 | Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to... | coqbot-app[bot] |
| 2021-03-25 | Merge PR #13852: [vernac] Improve alpha-renaming in record projection types | coqbot-app[bot] |
| 2021-03-23 | Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat... | Michael Soegtrop |
| 2021-03-23 | Merge PR #13914: Allow the presence of type casts for return values in Ltac2. | Michael Soegtrop |
| 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-03-16 | Adding a changelog and registering the new file in the documentation. | Pierre-Marie Pédrot |
| 2021-03-13 | Documenting the changes. | Pierre-Marie Pédrot |
| 2021-03-13 | Minimize the set of multiple inheritance paths to check for conversion | Kazuhiko Sakaguchi |
| 2021-03-12 | Fixed grammar productions for PDF documentations | Isaac Oscar Gariano |
| 2021-03-10 | Merge PR #13840: [notation] option to fine tune printing of literals | coqbot-app[bot] |
| 2021-03-10 | Add documentation. | Pierre-Marie Pédrot |
| 2021-03-10 | Regenerate the Ltac2 syntax for documentation. | Pierre-Marie Pédrot |
