aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* [Sphinx] Read version number from configureGravatar Maxime Dénès2018-03-13
|
* [Sphinx] Comment out metadata for unused backendsGravatar Maxime Dénès2018-03-13
|
* [Sphinx] Remove information for .chm backendGravatar Maxime Dénès2018-03-13
|
* [Sphinx] add bibliographyGravatar Maxime Dénès2018-03-13
|
* [Sphinx] Add indexesGravatar Maxime Dénès2018-03-13
|
* [Sphinx] Add table of contentsGravatar Maxime Dénès2018-03-12
|
* [Sphinx] Add doc preambleGravatar Maxime Dénès2018-03-12
|
* [Sphinx] Add a few grammar constructionsGravatar Maxime Dénès2018-03-12
| | | | Code from Paul Steckler (MIT).
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
| * Documentation for Cumulativity Weak Constraints.Gravatar Gaëtan Gilbert2018-03-09
| |
* | Merge PR #6480: Allow Prop as source for coercionsGravatar Maxime Dénès2018-03-09
|\ \ | |/ |/|
* | Merge PR #6818: Sphinx doc infrastructureGravatar Maxime Dénès2018-03-09
|\ \
| * | Moving Gitlab CI documentation build to the main Coq build.Gravatar Maxime Dénès2018-03-09
| | |
| * | Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.
* | | Merge PR #6895: [compat] Remove "Refolding Reduction" option.Gravatar Maxime Dénès2018-03-09
|\ \ \
* \ \ \ Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar Maxime Dénès2018-03-09
|\ \ \ \ | |_|/ / |/| | |
| | | * doc and changes for coercion from prop/typeGravatar charguer2018-03-09
| |_|/ |/| |
* | | Merge PR #6937: Add empty compat file for Coq 8.8Gravatar Maxime Dénès2018-03-09
|\ \ \
| | | * [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
| |_|/ |/| | | | | | | | | | | | | | | | | Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895.
* | | Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \
* \ \ \ Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6903: [compat] Remove "Shrink Abstract"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \
| | | | * | Add empty compat file for Coq 8.8Gravatar Jason Gross2018-03-07
| |_|_|/ / |/| | | | | | | | | | | | | | This closes #6598
* | | | | Remove outdated information regarding the FAQ.Gravatar Théo Zimmermann2018-03-06
| | | | | | | | | | | | | | | | | | | | The FAQ is not part of the Coq sources anymore.
| * | | | [compat] Remove "Shrink Abstract"Gravatar Emilio Jesus Gallego Arias2018-03-06
|/ / / / | | | | | | | | | | | | Following up on #6791, we the option "Shrink Abstract".
* | | | Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \
* \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \
| | | | | * | Deprecate Focus and Unfocus.Gravatar Théo Zimmermann2018-03-05
| | | | | | |
| | | * | | | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
| | * | | | Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| |/ / / / |/| | | |
* | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | supported scenarios.
| | | | | | * | Fix typos.Gravatar Théo Zimmermann2018-03-04
| |_|_|_|_|/ / |/| | | | | |
| | | | * | | [compat] Remove "Intuition Iff Unfolding"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Intuition Iff Unfolding"
| | | * | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| |_|/ / / |/| | | |
| | * | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| | | | | | | | | | | | | | | | | | | | Noticed by Sigurd Schneider.
| | | | * Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Gravatar Hugo Herbelin2018-02-28
| | | | |
| * | | | [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Parsing in `VernacLoad` was broken for a while, but the situation has improved by miscellaneous refactoring. However, we still cannot support `Load` properly when proofs are crossing file boundaries. So in this patch we do two things: - We check for supported scenarios [no proofs open at `Load` entry/exit] - Remove the hack in `toplevel` so the behavior of `Load` is consistent between `coqide`/`coqc`. We close #5053 as its main bug was fixed by the main toplevel refactoring and the remaining cases are documented now.
* / / / Typo in the documentation of the `pattern` tacticGravatar Joachim Breitner2018-02-27
|/ / /
* | | Merge PR #6819: Document Arguments extra scopes flagGravatar Maxime Dénès2018-02-24
|\ \ \
* \ \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ | |_|_|/ |/| | |
| | * | Document Arguments extra scopes flagGravatar Jasper Hugunin2018-02-22
| |/ / |/| |
| * | Doc: add Decimal-related files to index-list.html.templateGravatar Jason Gross2018-02-20
| | |
* | | Documenting use of primitive entry names for restricting syntax in notations.Gravatar Hugo Herbelin2018-02-20
| | |
* | | Extended documentation for notations referring to binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | Talking about the difference between ident and pattern. Giving examples.
* | | A first step at refreshing and documenting the new feature.Gravatar Hugo Herbelin2018-02-20
|/ /
| * Implement name mangling optionGravatar Jasper Hugunin2018-02-17
|/
* Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ | | | | | | information.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 16:33:22 +0000