aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* 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
|\ \ \
* \ \ \ 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
| | | | * Clarify further doc/README.md following Jim's comments.Gravatar Théo Zimmermann2018-06-22
| | | | * Fix copyright dates in doc/LICENSE.Gravatar Théo Zimmermann2018-06-22
| | | | * Improve doc/README.md.Gravatar Théo Zimmermann2018-06-22
| | | | * Move INSTALL.doc into doc/README.md.Gravatar Théo Zimmermann2018-06-22
| |_|_|/ |/| | |
* | | | 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 understa...Gravatar Maxime Dénès2018-06-21
|\ \ \ \ \
* \ \ \ \ \ 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
| | | | | | * 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
| | * | | | | [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
* | | | | | Fix #7829: Spurious documentation failures.Gravatar Théo Zimmermann2018-06-18
|/ / / / /
* | | | | 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 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
| |_|_|/ |/| | |
| | | * [doc] Disable smartquotes conversionGravatar Clément Pit-Claudel2018-06-08
| |_|/ |/| |
| | * 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
| | * 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
| | * [sphinx] Start fixing SSR chapter.Gravatar Théo Zimmermann2018-06-05
| |/ |/|
* | Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\ \
* \ \ Merge PR #7481: document 7025 (coq_makefile flag variables)Gravatar Maxime Dénès2018-06-04
|\ \ \
* \ \ \ Merge PR #7601: Fix notation for code snippet in documentationGravatar Maxime Dénès2018-06-04
|\ \ \ \ | |_|_|/ |/| | |
| | | * Documenting the deprecation.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|/ |/| |