aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Self-credit for the work done.Gravatar Théo Zimmermann2018-06-28
| | | | | | I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well.
* wrong sphinx syntaxGravatar Ambroise2018-06-28
|
* Update gallina-extensions.rstGravatar Ambroise2018-06-28
| | | I knew this feature existed but I did not remember the syntax and I could not find it in the manual
* Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\
* \ Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.Gravatar Maxime Dénès2018-06-26
|\ \
* \ \ Merge PR #7851: Modernize the introduction of the reference manual.Gravatar Maxime Dénès2018-06-26
|\ \ \
* \ \ \ Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \
| | | | * Documenting the syntax of mutual keywords.Gravatar Pierre-Marie Pédrot2018-06-24
| |_|_|/ |/| | |
* | | | Merge PR #7784: Remove Tutorials from a few other places following #7466.Gravatar Maxime Dénès2018-06-24
|\ \ \ \
* | | | | [ssr] document {}/viewGravatar Enrico Tassi2018-06-22
| | | | |
* | | | | [ssr] document rewrite {}fooGravatar Enrico Tassi2018-06-22
| | | | | | | | | | | | | | | | | | | | It was used in some examples, but never fully documented
| | | | * Clarify further doc/README.md following Jim's comments.Gravatar Théo Zimmermann2018-06-22
| | | | | | | | | | | | | | | | | | | | Relative links. Cf. #7800.
| | | | * Fix copyright dates in doc/LICENSE.Gravatar Théo Zimmermann2018-06-22
| | | | | | | | | | | | | | | | | | | | [ci skip]
| | | | * Improve doc/README.md.Gravatar Théo Zimmermann2018-06-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Fix the Markdown. - Add link to latest build of the refman for the master branch. - Clarify what are the dependencies of the HTML doc. [ci skip]
| | | | * Move INSTALL.doc into doc/README.md.Gravatar Théo Zimmermann2018-06-22
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | This will avoid in particular this ambiguous file extension. [ci skip]
* | | | Merge PR #7770: Move indices on top on the TOC. Closes #7764.Gravatar Maxime Dénès2018-06-21
|\ \ \ \
* \ \ \ \ Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵Gravatar Maxime Dénès2018-06-21
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | understands.
* \ \ \ \ \ Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.Gravatar Maxime Dénès2018-06-21
|\ \ \ \ \ \
| | | | | | * Mention Company-Coq as well.Gravatar Théo Zimmermann2018-06-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We put it in a footnote otherwise the sentence was starting to be really long. Footnotes need to be in index.rst to really appear at the bottom of the index page.
| | | | | | * Add a good reference for Proof-General as suggested by Clément.Gravatar Théo Zimmermann2018-06-20
| | | | | | |
| | | | | | * Modernize the introduction of the reference manual.Gravatar Théo Zimmermann2018-06-20
| |_|_|_|_|/ |/| | | | |
| | * | | | On cygwin, pass the filename in a format that coqdoc understands.Gravatar Jim Fehrle2018-06-20
| | | | | |
* | | | | | Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Gravatar Pierre-Marie Pédrot2018-06-19
|\ \ \ \ \ \
| | * | | | | [doc] Rewrite and document the prodn directiveGravatar Clément Pit-Claudel2018-06-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
| | * | | | | [doc] Fix a typo in the ssreflect chapterGravatar Clément Pit-Claudel2018-06-19
| | | | | | |
| | * | | | | [doc] Fix uncaught duplicate-label errors in the SSReflect chapterGravatar Clément Pit-Claudel2018-06-19
| | | | | | |
| | * | | | | [doc] Use productionlist instead of prodn in ring.rstGravatar Clément Pit-Claudel2018-06-19
| |/ / / / / |/| | | | |
| * | | | | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
* | | | | | Fix #7829: Spurious documentation failures.Gravatar Théo Zimmermann2018-06-18
|/ / / / / | | | | | | | | | | | | | | | We split a Require Import in two to avoid reaching the timeout.
* | | | | Merge PR #7848: Fix a typo in documentationGravatar Théo Zimmermann2018-06-17
|\ \ \ \ \
| | | | * | Remove Tutorial from Additional documentation in refman intro.Gravatar Théo Zimmermann2018-06-17
| | | | | |
| | | | * | Remove Tutorials from doc/LICENSE following #7466.Gravatar Théo Zimmermann2018-06-17
| |_|_|/ / |/| | | |
| | | * | Add introduction and credits to the TOC.Gravatar Théo Zimmermann2018-06-17
| | | | | | | | | | | | | | | | | | | | Move credits to its own chapter (closes #6573).
| | | * | Move indexes on top on the TOC. Closes #7764.Gravatar Théo Zimmermann2018-06-17
| |_|/ / |/| | |
* | | | Merge PR #7749: [doc] Disable smartquotes conversionGravatar Maxime Dénès2018-06-17
|\ \ \ \
* | | | | [sphinx] Finish clean-up of the Canonical Structure subsection.Gravatar Théo Zimmermann2018-06-16
| | | | |
* | | | | doc: Add "Print Canonical Projections" command to Command indexGravatar Anton Trunov2018-06-16
| |_|/ / |/| | |
| | * | doc: fix typo.Gravatar whitequark2018-06-13
| |/ / |/| |
* | | Merge PR #7284: [sphinx] Start fixing SSR chapter.Gravatar Maxime Dénès2018-06-11
|\ \ \
* \ \ \ Merge PR #7515: gitlab: build sphinx doc in separate jobGravatar Emilio Jesus Gallego Arias2018-06-09
|\ \ \ \
| * | | | gitlab: build sphinx doc in separate jobGravatar Gaëtan Gilbert2018-06-08
| | | | |
| | | | * Existing Class noop when already a class + warning.Gravatar Gaëtan Gilbert2018-06-08
| |_|_|/ |/| | | | | | | | | | | Fix #5012.
| | | * [doc] Disable smartquotes conversionGravatar Clément Pit-Claudel2018-06-08
| |_|/ |/| | | | | | | | Closes GH-7742.
| | * Improve links to SSR tactics, and some other improvements.Gravatar Théo Zimmermann2018-06-05
| | |
| | * Workaround a weird error of .. coqtop::Gravatar Théo Zimmermann2018-06-05
| | |
| | * Remove many abusive .. coqtop in SSR chapter.Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | Many still remain.
| | * A few additional small fixes.Gravatar Théo Zimmermann2018-06-05
| | |
| | * [sphinx] Fix missing indices warnings.Gravatar Théo Zimmermann2018-06-05
| | |
| | * [ssr] index entry for "without loss", "suffices" and "generally have"Gravatar Enrico Tassi2018-06-05
| | |
| | * [ssr] some fixes to the documentation markupGravatar Enrico Tassi2018-06-05
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 23:39:18 +0000