aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-06-09Minor improvements to the section on basics.Théo Zimmermann
2020-06-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-09Merge PR #12462: Summary of changes for 8.12Théo Zimmermann
2020-06-09Summary of changes for 8.12Matthieu Sozeau
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
2020-06-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-06-08Refactor SELF code for clarityJim Fehrle
2020-06-08Merge PR #12482: [ci] [overlays] Pin unicoq to a stable version.Théo Zimmermann
2020-06-08[ci] [overlays] Pin unicoq to a stable version.Emilio Jesus Gallego Arias
2020-06-08Merge PR #12480: Don't suggest Proof using when no section variablesEmilio Jesus Gallego Arias
2020-06-08Merge PR #12471: Fix uncaught NotArity in inductive typePierre-Marie Pédrot
2020-06-08Merge PR #12477: [sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform....Théo Zimmermann
2020-06-08Merge PR #12451: Fix Flocq build on Windows.Emilio Jesus Gallego Arias
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
2020-06-07[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_linesClément Pit-Claudel
2020-06-07Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: di...Clément Pit-Claudel
2020-06-06Match only a single line as the coqtop promptJim Fehrle
2020-06-06Merge PR #12380: Fix #12361 (indexing issues in the PDF)Théo Zimmermann
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
2020-06-05Fix Flocq build in Windows add-ons.Théo Zimmermann
2020-06-05Merge PR #12336: Factorize code in hint declaration.Hugo Herbelin
2020-06-05Merge PR #12450: Document known issue of Proof <term> with PG.Emilio Jesus Gallego Arias
2020-06-05Merge PR #12460: Add remaining 8.12+beta1 changelog entries.Emilio Jesus Gallego Arias
2020-06-05Merge PR #12459: Document incompatibility with Sphinx 3.Emilio Jesus Gallego Arias
2020-06-05Merge PR #12437: Fix ONLY_WINDOWS in .gitlab-ci.yml.Emilio Jesus Gallego Arias
2020-06-05Merge PR #12397: Fix #12280: do not use xindy to avoid build failures on some...Emilio Jesus Gallego Arias
2020-06-05Merge PR #12456: Fix version switcher when building with Dune.Emilio Jesus Gallego Arias
2020-06-05Adjust list of versions in version switcher.Théo Zimmermann
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-05Document incompatibility with Sphinx 3.Théo Zimmermann
2020-06-05Fix version switcher when building with Dune.Théo Zimmermann
2020-06-05Fix comment.Théo Zimmermann
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-05Merge PR #11707: Split the Reductionops machine from the cbn oneMaxime Dénès
2020-06-04Tweak wording.Théo Zimmermann
2020-06-04Document known issue of Proof <term> with PG.Théo Zimmermann
2020-06-04Merge PR #12440: [declare] Hide internals of variable declaration entries.Gaëtan Gilbert
2020-06-04Move the Cbn module to tactics/.Pierre-Marie Pédrot
2020-06-04Further cleanup.Pierre-Marie Pédrot
2020-06-04Move the cbn reduction to its own file, and simplify the RAKAM accordingly.Pierre-Marie Pédrot
2020-06-03Merge PR #12419: Various cleanups in eautoHugo Herbelin
2020-06-03[declare] Hide internals of variable declaration entries.Emilio Jesus Gallego Arias
2020-06-03Merge PR #12427: Add a dependency of coq_makefile's coqdep target into _CoqPr...Enrico Tassi
2020-06-03Merge PR #12337: Move CoqIDE to its own folderEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 18:13:21 +0000