Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Give advice on managing GitHub notifications in CONTRIBUTING. | Théo Zimmermann | 2018-05-14 |
| | |||
* | Merge PR #7278: pre-commit : do not fail miserably if git config has ↵ | Gaëtan Gilbert | 2018-04-17 |
|\ | | | | | | | `apply.whitespace = fix` | ||
| * | pre-commit : do not fail miserably if git config has `apply.whitespace = fix` | Pierre Letouzey | 2018-04-17 |
|/ | | | | | | | | | Having `--whitespace=` on all `git apply` in this script should make it insensitive to user setup in `~/.gitconfig`, at least `[apply] whitespace = fix`. Note that even this way, this script remains hugely fragile and non mature, and would better *not* be set by default for everybody. | ||
* | Merge PR #7277: Mention sphinxcontrib-bibtex in INSTALL.doc | Théo Zimmermann | 2018-04-17 |
|\ | |||
| * | Mention sphinxcontrib-bibtex in INSTALL.doc | Maxime Dénès | 2018-04-17 |
|/ | |||
* | Merge PR #7276: Add some 8.8.0 contributors in credits | Maxime Dénès | 2018-04-17 |
|\ | |||
| * | Add some 8.8.0 contributors in credits | Maxime Dénès | 2018-04-17 |
|/ | |||
* | Merge PR #7272: Mention other deprecations and fixes in CHANGES | Maxime Dénès | 2018-04-16 |
|\ | |||
* \ | Merge PR #7270: Sphinx doc fix indices | Maxime Dénès | 2018-04-16 |
|\ \ | |||
| * | | [Sphinx] Clean-up indices | Maxime Dénès | 2018-04-16 |
| | | | |||
* | | | Merge PR #7264: [Sphinx] Fix a lot of references and description of options | Maxime Dénès | 2018-04-16 |
|\| | | |||
* | | | Merge PR #7269: Protecting against a "deprecated cofix" warning. | Maxime Dénès | 2018-04-16 |
|\ \ \ | |||
* \ \ \ | Merge PR #7266: Remove LaTeX refman, now that migration to Sphinx is complete | Maxime Dénès | 2018-04-16 |
|\ \ \ \ | |||
| | | | * | Fix typo in CHANGES. | Maxime Dénès | 2018-04-16 |
| | | | | | |||
* | | | | | Merge PR #7225: Document the Export Set/Unset commands. | Maxime Dénès | 2018-04-16 |
|\ \ \ \ \ | |||
| | | | | * | Mention other deprecations and fixes in CHANGES | Maxime Dénès | 2018-04-16 |
| |_|_|_|/ |/| | | | | |||
| | | * | | Protecting against a "deprecated cofix" warning. | Hugo Herbelin | 2018-04-16 |
| | | | | | |||
| | * | | | Remove LaTeX refman, now that migration to Sphinx is complete | Maxime Dénès | 2018-04-16 |
| |/ / / |/| | | | |||
| | | * | [Sphinx] Fix a lot of references and description of options | Maxime Dénès | 2018-04-16 |
| | | | | |||
* | | | | Merge PR #7125: Adding ML headers in setoid_ring | Maxime Dénès | 2018-04-16 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7237: [ssr] fix delayed clears (fix #7045) | Maxime Dénès | 2018-04-16 |
|\ \ \ \ \ | |_|_|/ / |/| | | | | |||
* | | | | | Merge PR #7215: Deprecate the "simple subst" tactic. | Hugo Herbelin | 2018-04-16 |
|\ \ \ \ \ | |||
| | | | * | | Document the Export Set/Unset commands. | Pierre-Marie Pédrot | 2018-04-16 |
| |_|_|/ / |/| | | | | | | | | | | | | | | Fixes #6963. | ||
* | | | | | Merge PR #7263: CHANGES: document COQFLAGS change | Enrico Tassi | 2018-04-16 |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
| * | | | | CHANGES: document COQFLAGS change | Ralf Jung | 2018-04-16 |
|/ / / / | |||
* | | | | Merge PR #7200: [ltac] Deprecate nameless fix/cofix. | Maxime Dénès | 2018-04-16 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing | Maxime Dénès | 2018-04-16 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7246: Add missing CHANGES entry for #6169. | Maxime Dénès | 2018-04-16 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7247: Simplify CircleCI script | Gaëtan Gilbert | 2018-04-15 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #7252: Sphinx doc fix warnings | Théo Zimmermann | 2018-04-15 |
|\ \ \ \ \ \ \ \ | |||
| | * | | | | | | | Simplify CircleCI script | Yishuai Li | 2018-04-15 |
| |/ / / / / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #7250: Sphinx doc chapter 9 | Théo Zimmermann | 2018-04-14 |
|\ \ \ \ \ \ \ \ | |||
| | * | | | | | | | [Sphinx] Build with warnings as errors | Maxime Dénès | 2018-04-14 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Most of these warnings should really be errors (ill-formed input, invalid cross references, etc.) so we make it the default. | ||
| | * | | | | | | | [Sphinx] Fix all remaining warnings. | Maxime Dénès | 2018-04-14 |
| | | | | | | | | | |||
| | | | * | | | | | doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing | Clément Pit-Claudel | 2018-04-14 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Ubuntu Font License requires substantially modified fonts to be renamed entirely. | ||
| | * | | | | | | | [sphinx] Fix many warnings. | Théo Zimmermann | 2018-04-14 |
| |/ / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | ||
| * | | | | | | | [Sphinx] Add chapter 9. | Théo Zimmermann | 2018-04-14 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Chapter ported by Théo Zimmermann and Maxime Dénès. | ||
| * | | | | | | | [Sphinx] Move chapter 9 to new infrastructure. | Théo Zimmermann | 2018-04-14 |
|/ / / / / / / | |||
* | | | | | | | Merge PR #7136: Evar maps contain econstrs. | Pierre-Marie Pédrot | 2018-04-14 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #7217: Sphinx doc chapter 1 | Théo Zimmermann | 2018-04-14 |
|\ \ \ \ \ \ \ \ | |||
| | | * | | | | | | Add missing CHANGES entry for #6169. | Théo Zimmermann | 2018-04-14 |
| |_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | Fixes #7243. | ||
| | * | | | | | | Overlay for econstr in Evd. | Gaëtan Gilbert | 2018-04-13 |
| | | | | | | | | |||
| | * | | | | | | Evar maps contain econstrs. | Gaëtan Gilbert | 2018-04-13 |
| |/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr. | ||
* | | | | | | | Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵ | Pierre-Marie Pédrot | 2018-04-13 |
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | contains evars | ||
| | | | * | | | | [ltac] Deprecate nameless fix/cofix. | Emilio Jesus Gallego Arias | 2018-04-13 |
| |_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171. | ||
| | * | | | | | [Sphinx] Add Chapter 1 | Maxime Dénès | 2018-04-13 |
| | | | | | | | |||
| | * | | | | | [Sphinx] Move chapter 1 to new infrastructure | Maxime Dénès | 2018-04-13 |
| |/ / / / / |/| | | | | | |||
* | | | | | | Merge PR #7117: Sphinx doc chapter 29 | Théo Zimmermann | 2018-04-13 |
|\ \ \ \ \ \ | |||
| | | | | * | | [ssr] fix delayed clears (fix #7045) | Enrico Tassi | 2018-04-13 |
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | We take into account all future ipats, not just the ones in the current branch | ||
* | | | | | | Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods. | Enrico Tassi | 2018-04-13 |
|\ \ \ \ \ \ |