aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-23update CHANGESEnrico Tassi
2018-03-23Merge PR #7030: [default.nix] Add dependencies of the merging script.Vincent Laporte
2018-03-22Merge PR #7031: Owners for developer toolsThéo Zimmermann
2018-03-22Owners for developer toolsMaxime Dénès
2018-03-22Merge pull request #7040 from maximedenes/sphinx-doc-chapter-22Guillaume Melquiond
Sphinx doc chapter 22
2018-03-22Merge branch 'master' into sphinx-doc-chapter-22Guillaume Melquiond
2018-03-22Merge pull request #7039 from maximedenes/sphinx-doc-chapter-21Guillaume Melquiond
Sphinx doc chapter 21
2018-03-22Merge branch 'master' into sphinx-doc-chapter-21Guillaume Melquiond
2018-03-22Merge pull request #7038 from maximedenes/sphinx-doc-chapter-19Guillaume Melquiond
Sphinx doc chapter 19
2018-03-22Merge branch 'master' into sphinx-doc-chapter-19Guillaume Melquiond
2018-03-22Merge pull request #7036 from maximedenes/sphinx-doc-chapter-17Guillaume Melquiond
Sphinx doc chapter 17
2018-03-22Switch maintainers for documentationMaxime Dénès
Guillaume and I agreed to switch, as the new Sphinx infrastructure changes this component significantly.
2018-03-22bool option -> (VernacCumulative | VernacNonCumulative) optionGaëtan Gilbert
2018-03-22[Sphinx] Add chapter 22Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-03-22[Sphinx] Move chapter 22 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Add chapter 21Maxime Dénès
Thanks to Pierre Letouzey for porting this chapter.
2018-03-22[Sphinx] Move chapter 21 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Add chapter 19Maxime Dénès
Thanks to Laurent Théry for porting this chapter.
2018-03-22[Sphinx] Move chapter 19 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Add chapter 17Maxime Dénès
Thanks to Clément Pit-Claudel for porting this chapter.
2018-03-22[Sphinx] Move chapter 17 to new infrastructureMaxime Dénès
2018-03-21docsRalf Jung
2018-03-21Remove obsolete files from dev/docEnrico Tassi
- cic.dtd is related to the XML plugin - about-hints uses v7 syntax - minicoq.tex talks about a tool that is not there - translate.txt talks about the v7->v8 translation machinery - transition-* talk about v5->v7 changes to the sources layout
2018-03-21[default.nix] Add dependencies of the merging script.Théo Zimmermann
2018-03-21Merge PR #7027: Refine a bit the decentralized merging process.Théo Zimmermann
2018-03-21Switching owners for `META.coq`Maxime Dénès
2018-03-21Fix appveyor entry in CODEOWNERS.Maxime Dénès
2018-03-21Refine a bit the decentralized merging process.Maxime Dénès
We make GitHub assign only principal maintainers as reviewers. This reduces the level of noise (PRs with 10 code owners), and makes it easy for the assignee to check if all reviews have been completed (all reviewers in the list have to approve the PR, which was not the case before if two reviewers were assigned for the same component). This change means that when a principal maintainer submits a patch touching the component they own, they should ask a review from the secondary maintainer.
2018-03-21Merge PR #7023: [ssreflect] Respect Opaque in FO unificationEnrico Tassi
2018-03-21Make parsing independent of the cumulativity flag.Gaëtan Gilbert
2018-03-21Fix #7026: ssr: applying an overloaded lemma as a view takes too long.Pierre-Marie Pédrot
Ssreflect was using a very complex function performing amongst other things refolding to check that a term was an applied inductive type. It now relies on a simple reduction followed by term matching.
2018-03-20Refactor impargs code.Jasper Hugunin
This should preserve semantics exactly. In the compute_implicits family of functions, I changed the name of the pushed rel to not be fresh, but the env isn't passed to find_displayed_name_in, and shouldn't affect whd_all.
2018-03-20coq_makefile: provide variables to override for adding extra flagsRalf Jung
2018-03-20coq_makefile: FLAG make variables should not contain LIBSRalf Jung
2018-03-20[ssreflect] Respect Opaque in FO unificationMaxime Dénès
2018-03-20Merge PR #7022: Update CODEOWNERSMaxime Dénès
2018-03-20Update CODEOWNERSEnrico
2018-03-20Merge PR #7014: New merging processMaxime Dénès
The last merge with the centralized process ;)
2018-03-20Add CODEOWNERSMaxime Dénès
See https://help.github.com/articles/about-codeowners/ for documentation.
2018-03-19Describe new merging process.Maxime Dénès
2018-03-19Fix typo in CHANGES.Théo Zimmermann
[skip ci]
2018-03-16Merge PR #7007: Emergency fix for OSX packaging job on Travis.Maxime Dénès
2018-03-16Merge PR #7000: win: update bignums to tag V8.8-beta.1Maxime Dénès
2018-03-16Merge PR #7006: [Sphinx] Add chapter 11Maxime Dénès
2018-03-16Merge PR #7005: Fix coqtop timeoutMaxime Dénès
2018-03-16Emergency fix for OSX packaging job on Travis.Maxime Dénès
Updates to homebrew packages can currently make this packaging job fail at any stage of the release cycle. Also, we are leaving dangerously because we depend on python2 and python3 at the same time, which is not supported by homebrew. To make this more reliable, we should switch to a Nix-based build infrastructure at least for macOS.
2018-03-16[Sphinx] Add chapter 11Maxime Dénès
Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot for porting this chapter.
2018-03-16Merge PR #7003: 8.8 changesMaxime Dénès
2018-03-16[Sphinx] Better error message for coqtop errorsMaxime Dénès
2018-03-16[Sphinx] Increase coqtop timeout to avoid spurious failures on CIMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 18:48:16 +0000