| Age | Commit message (Expand) | Author |
|---|
| 2020-05-03 | Further port of the SSR tactics. | Pierre-Marie Pédrot |
| 2020-05-03 | Further port of the SSR code. | Pierre-Marie Pédrot |
| 2020-05-03 | Export new combinators in SSR not relying on the legacy API. | Pierre-Marie Pédrot |
| 2020-05-03 | Further porting of ssrcode. | Pierre-Marie Pédrot |
| 2020-05-03 | Slightly more tricky port of the ssr tactics. | Pierre-Marie Pédrot |
| 2020-05-03 | Export missing tacticals. | Pierre-Marie Pédrot |
| 2020-05-03 | Further port SSReflect tactics to the new engine. | Pierre-Marie Pédrot |
| 2020-05-03 | Wrap ssr tactics into V82.tactic. | Pierre-Marie Pédrot |
| 2020-05-03 | Wrap a monadic combinator in a try-with block to catch exceptions. | Pierre-Marie Pédrot |
| 2020-05-03 | Remove a call to V82.tactic in Btauto. | Pierre-Marie Pédrot |
| 2020-05-03 | Remove a very specific low-level tactical from Refiner. | Pierre-Marie Pédrot |
| 2020-05-03 | Wrap Refiner.refiner in the tactic monad. | Pierre-Marie Pédrot |
| 2020-05-03 | Remove a critical call to V82.tactic in Clenvtac. | Pierre-Marie Pédrot |
| 2020-05-02 | Merge PR #12172: Refactor first chapter: first step, the section on basics. | Clément Pit-Claudel |
| 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-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 | [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 | Merge PR #12208: Reduce rational numbers in Cauchy real addition, to accelera... | Michael Soegtrop |
| 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 |
