| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.
|
|
|
|
|
|
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
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>
|
|
|
|
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
|
|
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
|
|
|
|
|
|
|
|
Closes GH-8482.
|
|
|
|
Also remove a few undocumented settings
|
|
|
|
to fix all misuses.
|
|
Remove objects without body from most chapters.
The remaining problems are all in the SSReflect chapter.
|
|
Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:
|
|
|
|
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
|
|
and field' chapters of the Reference Manual.
|
|
In particular, remove trailing dots.
|
|
|
|
- Remove all trailing dots.
- There is only one Bullet Behavior option.
- Replaces `@natural` and `@integer` by `@num`.
|
|
Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.
|
|
Thanks to Pierre Letouzey for porting this chapter.
|
|
|
