aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-26Add Michael Soegtrop as a code owner for Windows build scripts.Théo Zimmermann
2018-03-26Use Pierre Corbineau GitHub nickname in CODEOWNERS.Théo Zimmermann
2018-03-26More efficient reallocation of VM global tables.Pierre-Marie Pédrot
The previous code was mimicking what the C implementation was doing, which was a quadratic algorithm. We simply use the good old exponential reallocation strategy that is amortized O(1).
2018-03-26Moving the VM global atom table to a ML reference.Pierre-Marie Pédrot
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2018-03-25Clarify wording in tactics documentation.Théo Zimmermann
Closes #6980.
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
For instance, error in "Goal forall a f, f a = 0" is now located.
2018-03-23Deprecate undocumented "intros until 0" in favor of "intros *".Hugo Herbelin
- The case 0 makes the code of intros until (and in particular of Detyping.lookup_quantified_hypothesis_as_displayed more complicated). - The introduction pattern "*" is compositional while "until 0" is not.
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-11 20:15:08 +0000