aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-28Getting rid of some false "collision between bound variable names" warnings.Hugo Herbelin
- In a situation like "match x with ... end" with no "return" clause we don't warn for the implicit "as x" coming from repeating "x" - In a multiple fixpoint, we don't warn for the recursive context being distributed several times over the different mutual components.
2018-03-23Merge PR #7046: Switch maintainers for documentationThéo Zimmermann
2018-03-23Merge PR #7018: Fix typo in CHANGES.Maxime Dénès
2018-03-23Merge PR #7029: improve merge-pr scriptMaxime Dénès
2018-03-23improve merge-pr scriptEnrico Tassi
The script now performs many more checks and reports errors in a more intelligible way.
2018-03-23Merge PR #7052: More precise wording about the merge process.Théo Zimmermann
2018-03-23More precise wording about the merge process.Maxime Dénès
In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases.
2018-03-23Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ↵Enrico Tassi
too long.
2018-03-23Merge PR #6968: [stm] Never consider `Backtrack` as part of the script.Enrico Tassi
2018-03-23Merge PR #7025: Coq makefile: provide variables to extend the flags passed ↵Enrico Tassi
to coq, coqchk, coqdoc
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-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-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-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-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