aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-06-05[sphinx] Fix #12361Clément Pit-Claudel
2020-06-05[sphinx] Improve the error message printed for duplicate namesClément Pit-Claudel
2020-06-05[sphinx] Get rid of anonymous targets (Sphinx 2.3.1 doesn't like them)Clément Pit-Claudel
2020-06-05[sphinx] Remove most pylint warningsClément Pit-Claudel
2020-06-02Merge PR #12412: Reduce options passed to workersEnrico Tassi
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not depre...Emilio Jesus Gallego Arias
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
2020-06-01Merge PR #12422: Fixes #12418: an assert false in inference of return clauseEmilio Jesus Gallego Arias
2020-06-01Merge PR #12431: [ci] Split fiat-crypto into non-OCaml and OCamlGaëtan Gilbert
2020-05-31[ci] Split fiat-crypto into non-OCaml and OCamlJason Gross
2020-05-29Merge PR #12393: [declare] Miscellaneous nits from my main dev treeGaëtan Gilbert
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-29Change log for #12422.Hugo Herbelin
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
2020-05-29Merge PR #12421: Fixes for compilation without native dynlinkEmilio Jesus Gallego Arias
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-28Fixing compilation with -natdynlink no.Hugo Herbelin
2020-05-27Merge PR #12389: Small coq_makefile improvement.Enrico Tassi
2020-05-27Adding changelog.Martin Bodin
2020-05-27Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters s...Martin Bodin
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27[changelog/8.12] Wording improvements.Théo Zimmermann
2020-05-27[changelog/8.12] Use sections and provide a local TOC.Théo Zimmermann
2020-05-27[changelog/8.12] Split misc entries out in more relevant sections.Théo Zimmermann
2020-05-27Changelog entries for the 8.12 changes to the reference manual.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-27Fix changelog for #11986.Théo Zimmermann
2020-05-27Merge PR #12408: Fix output tests for location errors when running in async m...Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Factor common universe computation in close proof.Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_deferred in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Factor out universe computation in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Nit on errors.Emilio Jesus Gallego Arias
2020-05-26[declare] Turn restrict_ucontext hack into an internal parameterEmilio Jesus Gallego Arias
2020-05-26[nit] Remove unused exported error message in obligationsEmilio Jesus Gallego Arias
2020-05-26[declare] Don't expose internal parameter oblsEmilio Jesus Gallego Arias
2020-05-26[declare] Simplify exported type of definition_entryEmilio Jesus Gallego Arias
2020-05-26Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugsGaëtan Gilbert
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
2020-05-26Fix usage of -rifrom, -refrom.Théo Zimmermann
2020-05-26Fix worker handling of command-line options that are already included in init...Théo Zimmermann
2020-05-26Remove command-line options that do not exist anymore.Théo Zimmermann
2020-05-25dev/tools/make-changelog.sh now asks about fixed bugsJason Gross
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
2020-05-25Merge PR #12403: Fix hyperlinks in changes.rstThéo Zimmermann
2020-05-25Add a changelog.Pierre-Marie Pédrot
2020-05-25Remove the prolog tactic.Pierre-Marie Pédrot