aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools
AgeCommit message (Collapse)Author
2018-12-04Document undocumented flags and optionsJim Fehrle
Also remove a few undocumented settings
2018-10-11Documenting -arg in _CoqProject.Hugo Herbelin
We follow Proof General documentation, section 11.2 "Using the Coq project file".
2018-10-02[doc] Nits on utilities / toplevel building.Emilio Jesus Gallego Arias
2018-09-23Documentation for proof diffsJim Fehrle
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Fix a few LaTeX mistakesClément Pit-Claudel
2018-09-11building-a-coq-project-with-coq-makefile:fix typosJason Gross
make make-pretty-timed- after -> make make-pretty-timed-after (remove space between - and after) (and reflow paragraph) Fix spacing around :: in print-pretty-single-time-diff Closes #8396
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-28Merge PR #8281: Trivial Sphinx fix in doc.Clément Pit-Claudel
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-21Trivial Sphinx fix in doc.Théo Zimmermann
2018-08-02Merge PR #8143: Improved grammar and spelling in chapters 'Proof Schemes' ↵Théo Zimmermann
and 'The Coq commands' of the Reference Manual.
2018-08-02Merge PR #8144: Improved grammar and spelling for chapters 'Utilities' and ↵Théo Zimmermann
'CoqIDE' of the Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq ↵Zeimer
commands' of the Reference Manual.
2018-08-01Improved grammar and spelling for chapters 'Utilities' and 'CoqIDE' of the ↵Zeimer
Reference Manual.
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
2018-07-27Missing backslash in the documentation file.Martin Bodin
2018-07-08Remove Emacs modes.Théo Zimmermann
They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
2018-06-25Archive the `gallina` toolVincent Laporte
2018-06-04Merge PR #7481: document 7025 (coq_makefile flag variables)Maxime Dénès
2018-05-16Minor update of the documentation/man about the resource file.Hugo Herbelin
2018-05-16document 7025Enrico Tassi
2018-05-05[sphinx] Fix a porting mistake.Théo Zimmermann
2018-05-05[sphinx] Fix a typo that appeared during the migration.Théo Zimmermann
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14[sphinx] Fix many warnings.Théo Zimmermann
Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
2018-04-11[sphinx] Use macro |CoqIDE| consistently.Théo Zimmermann
2018-04-10[Sphinx] Add chapter 15Laurent Théry
Thanks to Laurent Théry for porting this chapter.
2018-04-10[Sphinx] Move chapter 15 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 16Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-03-15[Sphinx] Move chapter 16 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 14Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-03-15[Sphinx] Move chapter 14 to new infrastructureMaxime Dénès