Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | [Sphinx] Move chapter 26 to new infrastructure | 2018-03-29 | |
| | |||
* | [Sphinx] Add chapter 24 | 2018-03-29 | |
| | | | | Thanks to Matthieu Sozeau for porting this chapter. | ||
* | [Sphinx] Move chapter 24 to new infrastructure | 2018-03-29 | |
| | |||
* | [Sphinx] Add chapter 23 | 2018-03-29 | |
| | | | | Thanks to Pierre Letouzey for porting this chapter. | ||
* | [Sphinx] Move chapter 23 to new infrastructure | 2018-03-29 | |
| | |||
* | [Sphinx] Remove duplicate entry for command `Coercion` | 2018-03-29 | |
| | |||
* | [Sphinx] Add chapter 18 | 2018-03-29 | |
| | | | | Thanks to Pierre Letouzey for porting this chapter. | ||
* | [Sphinx] Move chapter 18 to new infrastructure | 2018-03-29 | |
| | |||
* | Merge PR #7057: Sphinx Chapter 20: Type Classes | 2018-03-29 | |
|\ | |||
* \ | Merge PR #7072: Update codeowners | 2018-03-29 | |
|\ \ | |||
| * | | Remove dev/doc/changes.md from files with a code owner. | 2018-03-29 | |
| | | | | | | | | | | | | | | | | | | 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. | ||
* | | | Merge PR #7090: stm: don't propagate side effects when editing a proof | 2018-03-28 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6961: [test-suite] Add backtracking test for `Load`. | 2018-03-28 | |
|\ \ \ \ | |||
| | * | | | stm: don't propagate side effects when editing a proof | 2018-03-27 | |
| | | | | | |||
* | | | | | Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *" | 2018-03-27 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7062: Slightly refining some error messages about unresolvable evars. | 2018-03-27 | |
|\ \ \ \ \ \ | |||
| | | | | | * | [doc] Port Chapter 20 Type Classes to Sphinx | 2018-03-26 | |
| | | | | | | | |||
* | | | | | | | Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵ | 2018-03-26 | |
|\ \ \ \ \ \ \ | |_|_|_|/ / / |/| | | | | | | | | | | | | | AppVeyor fail. | ||
| | | | | | * | Move Classes.tex to type-classes.rst | 2018-03-26 | |
| | | | | | | | |||
* | | | | | | | Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer. | 2018-03-26 | |
|\ \ \ \ \ \ \ | |||
| | | | | | * | | Add Michael Soegtrop as a code owner for Windows build scripts. | 2018-03-26 | |
| | | | | | | | | |||
| | | | | | * | | Use Pierre Corbineau GitHub nickname in CODEOWNERS. | 2018-03-26 | |
| |_|_|_|_|/ / |/| | | | | | | |||
| | | * | | | | Slightly refining some error messages about unresolvable evars. | 2018-03-24 | |
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | For instance, error in "Goal forall a f, f a = 0" is now located. | ||
| | | * | | | Deprecate undocumented "intros until 0" in favor of "intros *". | 2018-03-23 | |
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | - 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. | ||
* | | | | | Merge PR #7046: Switch maintainers for documentation | 2018-03-23 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7018: Fix typo in CHANGES. | 2018-03-23 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7029: improve merge-pr script | 2018-03-23 | |
|\ \ \ \ \ \ \ | |||
| * | | | | | | | improve merge-pr script | 2018-03-23 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The script now performs many more checks and reports errors in a more intelligible way. | ||
* | | | | | | | | Merge PR #7052: More precise wording about the merge process. | 2018-03-23 | |
|\ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ |/| | | | | | | | |||
| * | | | | | | | More precise wording about the merge process. | 2018-03-23 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases. | ||
* | | | | | | | | Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ↵ | 2018-03-23 | |
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | too long. | ||
* \ \ \ \ \ \ \ \ | Merge PR #6968: [stm] Never consider `Backtrack` as part of the script. | 2018-03-23 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7025: Coq makefile: provide variables to extend the flags passed ↵ | 2018-03-23 | |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | to coq, coqchk, coqdoc | ||
| * | | | | | | | | | | update CHANGES | 2018-03-23 | |
| | | | | | | | | | | | |||
* | | | | | | | | | | | Merge PR #7030: [default.nix] Add dependencies of the merging script. | 2018-03-23 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7031: Owners for developer tools | 2018-03-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | |||
| * | | | | | | | | | | | Owners for developer tools | 2018-03-22 | |
|/ / / / / / / / / / / | |||
* | | | | | | | | | | | Merge pull request #7040 from maximedenes/sphinx-doc-chapter-22 | 2018-03-22 | |
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | Sphinx doc chapter 22 | ||
| * \ \ \ \ \ \ \ \ \ \ | Merge branch 'master' into sphinx-doc-chapter-22 | 2018-03-22 | |
| |\ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / |/| | | | | | | | | | | | |||
* | | | | | | | | | | | | Merge pull request #7039 from maximedenes/sphinx-doc-chapter-21 | 2018-03-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | Sphinx doc chapter 21 | ||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'master' into sphinx-doc-chapter-21 | 2018-03-22 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / |/| | | | | | | | | | | | | |||
* | | | | | | | | | | | | | Merge pull request #7038 from maximedenes/sphinx-doc-chapter-19 | 2018-03-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Sphinx doc chapter 19 | ||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'master' into sphinx-doc-chapter-19 | 2018-03-22 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | Merge pull request #7036 from maximedenes/sphinx-doc-chapter-17 | 2018-03-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Sphinx doc chapter 17 | ||
| | | | | | | | | | | * | | | | Switch maintainers for documentation | 2018-03-22 | |
| |_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Guillaume and I agreed to switch, as the new Sphinx infrastructure changes this component significantly. | ||
| | | | * | | | | | | | | | | [Sphinx] Add chapter 22 | 2018-03-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Thanks to Paul Steckler for porting this chapter. | ||
| | | | * | | | | | | | | | | [Sphinx] Move chapter 22 to new infrastructure | 2018-03-22 | |
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | |||
| | | * | | | | | | | | | | [Sphinx] Add chapter 21 | 2018-03-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Thanks to Pierre Letouzey for porting this chapter. | ||
| | | * | | | | | | | | | | [Sphinx] Move chapter 21 to new infrastructure | 2018-03-22 | |
| |_|/ / / / / / / / / / |/| | | | | | | | | | | | |||
| | * | | | | | | | | | | [Sphinx] Add chapter 19 | 2018-03-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Thanks to Laurent Théry for porting this chapter. |