| Age | Commit message (Expand) | Author |
|---|
| 2020-05-01 | Changing fixpoint message "decreasing" -> "guarded". | Hugo Herbelin |
| 2020-05-01 | Fixing #11903: Fixpoints not truly recursive in standard library. | Hugo Herbelin |
| 2020-05-01 | Warn when a (co)fixpoint is not truly recursive. | Hugo Herbelin |
| 2020-05-01 | Slight modification of the partial-order algorithm so that it does not | Hugo Herbelin |
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann |
| 2020-05-01 | Merge PR #12221: Replace QSeqEquiv by QCauchySeq, simplify proofs. | Michael Soegtrop |
| 2020-05-01 | Preserve vernac chapter. | Théo Zimmermann |
| 2020-05-01 | Extract two new files out of Gallina chapter. | Théo Zimmermann |
| 2020-05-01 | Create section on writing libraries with only deprecated attributes. | Théo Zimmermann |
| 2020-05-01 | Extract deprecated attribute from Gallina chapter. | Théo Zimmermann |
| 2020-05-01 | Remove flags, options and tables from vernac chapter. | Théo Zimmermann |
| 2020-05-01 | Remove lexical conventions and attributes from Gallina chapter. | Théo Zimmermann |
| 2020-05-01 | Create basics out of sections from Gallina and Vernac chapters. | Théo Zimmermann |
| 2020-05-01 | Create section on basics with just flags, options and tables. | Théo Zimmermann |
| 2020-05-01 | Extract flags, options and tables from vernac chapter. | Théo Zimmermann |
| 2020-05-01 | Create section on basics with just lexical conventions and attributes. | Théo Zimmermann |
| 2020-05-01 | Extract lexical conventions and attributes from Gallina chapter. | Théo Zimmermann |
| 2020-05-01 | Merge PR #12217: Fix #12215: ci scripts naming inconsistencies | Emilio Jesus Gallego Arias |
| 2020-05-01 | Merge PR #12222: Less confusing configure message when lablgtk exists but not... | Emilio Jesus Gallego Arias |
| 2020-05-01 | do not re-export ListNotations from Program: vst overlay | Antonio Nikishaev |
| 2020-04-30 | Replace QSeqEquiv by QCauchySeq, simplify proofs. | Vincent Semeria |
| 2020-04-30 | Less confusing configure message when lablgtk exists but not lablgtksourceview. | Hugo Herbelin |
| 2020-04-30 | Merge PR #12213: [zify] add support for Nat.le, Nat.lt and Nat.eq | Vincent Laporte |
| 2020-04-30 | renaming in Makefile.ci and ci scripts to avoid inconsistencies | Olivier Laurent |
| 2020-04-30 | Merge PR #12216: Remove outdated code and comments in Declare. | Emilio Jesus Gallego Arias |
| 2020-04-30 | Move availability_of_prim_token | Pierre Roux |
| 2020-04-30 | [zify] add support for Nat.le, Nat.lt and Nat.eq | Frédéric Besson |
| 2020-04-30 | Merge PR #12107: Remove mod_constraints field of module body | Pierre-Marie Pédrot |
| 2020-04-30 | Remove outdated code and comments in Declare. | Pierre-Marie Pédrot |
| 2020-04-30 | Symmetry in conclusions of List.map_eq_* | Olivier Laurent |
| 2020-04-30 | Merge PR #12208: Reduce rational numbers in Cauchy real addition, to accelera... | Michael Soegtrop |
| 2020-04-30 | do not re-export ListNotations from Program: fix testsuite | Antonio Nikishaev |
| 2020-04-30 | do not re-export ListNotations from Program: changelog | Antonio Nikishaev |
| 2020-04-30 | do not re-export ListNotations from Program: overlays | Antonio Nikishaev |
| 2020-04-30 | do not re-export ListNotations from Program | Antonio Nikishaev |
| 2020-04-29 | When TIMED=1, emit timing info for OCaml files | Jason Gross |
| 2020-04-29 | Merge PR #12209: Merge duplicates in .mailmap | Théo Zimmermann |
| 2020-04-29 | Merge duplicates in .mailmap | Jason Gross |
| 2020-04-29 | Reduce rational numbers in Cauchy real addition, to accelerate it | Vincent Semeria |
| 2020-04-29 | Merge PR #11606: [tools] Add memory stats to tables by default | Emilio Jesus Gallego Arias |
| 2020-04-29 | Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ... | Emilio Jesus Gallego Arias |
| 2020-04-29 | Merge PR #12198: CI: change ext-lib url, it is at coq-community now | Emilio Jesus Gallego Arias |
| 2020-04-29 | Merge PR #12202: Centralize the call to `tclEFFECTS` in scheme declaration | Emilio Jesus Gallego Arias |
| 2020-04-29 | Merge PR #12150: Support in-line glossary definitions and references with an ... | Clément Pit-Claudel |
| 2020-04-29 | Merge PR #12158: [univ] API to demote global universes | Matthieu Sozeau |
| 2020-04-29 | Merge PR #12195: [doc] [sphinx] Run in silent mode by default | Théo Zimmermann |
| 2020-04-29 | Merge PR #12174: [ci] Add coq-tools to the CI | Théo Zimmermann |
| 2020-04-29 | Support in-line glossary entries and references | Jim Fehrle |
| 2020-04-29 | Merge PR #12203: [ci] [doc] misspelled script name create_overlays.sh | Théo Zimmermann |
| 2020-04-29 | [univ] API to demote global universes | Enrico Tassi |
