coq/doc/sphinx/using/tools, branch master The formal proof system Convert rewriting and proof-mode chapters to prodn 2020-12-30T19:48:37+00:00 Jim Fehrle 2020-09-13T03:54:22+00:00 e02120ed6580733db2276f0c11b4f432ea670ee3 






Documenting one-line verbatim.
2020-11-14T21:55:47+00:00

Hugo Herbelin

2020-11-05T12:17:38+00:00

0b12bb8c03b0ac7cc8aa7578a8db8ca93ecd1fd0












[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.
2020-11-09T17:39:49+00:00

Théo Zimmermann

2020-11-09T17:39:49+00:00

a3869e5371c89629ddfd8ccdd1bdc0de12efe806

The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.





The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.







Add some missing smallcaps.
2020-10-20T09:07:52+00:00

Théo Zimmermann

2020-10-19T14:06:30+00:00

3230c568eb0bc719feca642a1537555e262478eb












Add index for coqdoc.
2020-06-21T15:49:14+00:00

Théo Zimmermann

2020-06-21T15:49:14+00:00

5f9572b4b6280995b5c1078f59f7f514e665a4c0

Fixes #12545.





Fixes #12545.







Release notes for 8.12.
2020-05-27T13:38:24+00:00

Théo Zimmermann

2020-05-23T10:58:37+00:00

2f0a89e59e615e6101096b36e12e7b7bbace8eff












coqdoc: Add (* begin details *) and (* end details *)
2020-03-28T15:53:38+00:00

Thomas Letan

2019-07-27T11:26:17+00:00

86d5ed1d96a93c074a070c86b1c3c81088e4cd2d

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.





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.







Split coqdoc section out of utility chapter (octopus merge).
2020-03-27T13:19:48+00:00

Théo Zimmermann

2020-03-27T13:19:48+00:00

223ccc1dcf9a0fd0ba3b82f910b507926affe1a2

This octopus merge is meant to preserve the commit history / blame of
both parts.





This octopus merge is meant to preserve the commit history / blame of
both parts.







Move section on coqdoc to new location.
2020-03-27T13:18:52+00:00

Théo Zimmermann

2020-03-27T13:11:20+00:00

4da3fe8aafe2d5ceadb505ba16cfbb4482755c61












[refman] Move chapters into new structure.
2020-03-19T14:51:22+00:00

Théo Zimmermann

2020-02-13T17:47:42+00:00

f5be988da566d0a48c67bd81be6d32376b3ba2a5

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>





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>