aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/using
AgeCommit message (Collapse)Author
2021-03-10Add documentation.Pierre-Marie Pédrot
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-14Documenting one-line verbatim.Hugo Herbelin
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-09-11[refman] Rename num to naturalPierre Roux
2020-06-21Add index for coqdoc.Théo Zimmermann
Fixes #12545.
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-16Fix note on implicit arguments in doc of functional induction.Théo Zimmermann
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-05-01Create section on writing libraries with only deprecated attributes.Théo Zimmermann
2020-04-23[refman] Fix name of tactic: function induction -> functional induction.Théo Zimmermann
2020-04-21Merge all documentation on Funind into the same file.Théo Zimmermann
2020-04-21Consolidate funind tactics and Functional Scheme in Funind section of the ↵Théo Zimmermann
Libraries chapter.
2020-04-21Extract funind tactics to funind section of the Libraries chapter.Théo Zimmermann
2020-04-20Move Functional Scheme to Funind section.Théo Zimmermann
2020-04-03Move section on funind in appropriate location (inside libraries).Théo Zimmermann
2020-03-28coqdoc: Add (* begin details *) and (* end details *)Thomas Letan
We propose to add an environment to have foldable texts with HTML output, more precisely: (*begin details [: An optional summary] *) some Coq and documentation material (* end details *) Currently, only the HTML output is supported. We could treat this environment in LaTeX output as appendixes to output later.
2020-03-27Split coqdoc section out of utility chapter (octopus merge).Théo Zimmermann
This octopus merge is meant to preserve the commit history / blame of both parts.
2020-03-27Move section on coqdoc to new location.Théo Zimmermann
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: https://github.com/coq/ceps/pull/43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:02:49 +0000