aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-31Merge PR #7130: gitlab: fix environment for build templateEmilio Jesus Gallego Arias
2018-03-30gitlab: fix environment for build templateGaëtan Gilbert
When `build` was made to build the doc it dropped `-coqide opt` and dropped the environment variables for building coqide. The combination means that when the cache had lablgtk in opam (installed by some other job) configure would pick it up but the system package wouldn't be there causing a failure. When lablgtk isn't in the cache everything was fine.
2018-03-29Merge PR #7057: Sphinx Chapter 20: Type ClassesMaxime Dénès
2018-03-29Merge PR #7072: Update codeownersMaxime Dénès
2018-03-29Remove dev/doc/changes.md from files with a code owner.Théo Zimmermann
Like CHANGES, and the test-suite folder, this file receives too many updates to have a code owner. It is the job of the reviewer of the PR to review changes to these files as well.
2018-03-28Merge PR #7090: stm: don't propagate side effects when editing a proofEmilio Jesus Gallego Arias
2018-03-28Merge PR #6961: [test-suite] Add backtracking test for `Load`.Enrico Tassi
2018-03-27stm: don't propagate side effects when editing a proofEnrico Tassi
2018-03-27Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *"Pierre-Marie Pédrot
2018-03-27Merge PR #7062: Slightly refining some error messages about unresolvable evars.Pierre-Marie Pédrot
2018-03-26[doc] Port Chapter 20 Type Classes to SphinxMatthieu Sozeau
2018-03-26Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵Maxime Dénès
AppVeyor fail.
2018-03-26Move Classes.tex to type-classes.rstMatthieu Sozeau
2018-03-26Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Enrico Tassi
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:31:57 +0000