| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 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-09-11 | [refman] Rename num to natural | Pierre Roux | |
| 2020-09-11 | Remove outdated references to productionlist. | Théo Zimmermann | |
| 2020-05-18 | Support :gdef:`text <term>` syntax (adding "<term>") | Jim Fehrle | |
| 2020-04-29 | Support in-line glossary entries and references | Jim Fehrle | |
| with an index | |||
| 2020-03-09 | Remove some productionlists | Jim Fehrle | |
| 2020-02-28 | Convert Gallina Vernac to use prodn | Jim Fehrle | |
| 2019-12-28 | Convert productionlists to prodns | Jim Fehrle | |
| 2019-12-14 | Make prodn look more like productionlist | Jim Fehrle | |
| 2019-07-01 | Update doc for % escapes in Sphinx doc, improve error messages | Jim Fehrle | |
| 2019-05-16 | [refman] Introduce syntax for alternatives in notations | Clément Pit-Claudel | |
| Closes GH-8482. | |||
| 2019-02-28 | [sphinx] Add warn option to coqtop directive. | Théo Zimmermann | |
| By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected. | |||
| 2019-02-19 | [sphinx] Refactor handling of options for coqtop directive. | Théo Zimmermann | |
| Make it mandatory to give exactly one display option. | |||
| 2019-02-18 | [sphinx] Add abort and restart options to directive coqtop. | Théo Zimmermann | |
| 2019-02-18 | Sphinx: fail when a command fails | Gaëtan Gilbert | |
| This uses a new coqtop-only option "Coqtop Exit On Error", not sure where to put the doc for it. It being an option means we can locally turn it off (.. coqtop:: fail). | |||
| 2019-02-18 | Sphinx: remove [coqtop:: undo] | Gaëtan Gilbert | |
| Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2019-02-18 | Add diff rule for README.rst to dune refman-html alias | Gaëtan Gilbert | |
| We change regen_readme such that when given an argument it outputs there instead of overwriting the readme. Prompted by me noticing I forgot to regen in #9553. | |||
| 2019-01-23 | Move and rewrite documentation for intro patterns that was under | Jim Fehrle | |
| the intros tactic to its own subsection. Add grammar and examples. | |||
| 2018-12-03 | Closes #9118: single backticks are made equivalent to double backticks; try ↵ | Théo Zimmermann | |
| to fix all misuses. | |||
| 2018-10-01 | Merge PR #8301: Documentation for proof diffs | Théo Zimmermann | |
| 2018-09-25 | [doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJax | Clément Pit-Claudel | |
| 2018-09-23 | Update flag, option and table descriptions in coqdomain.py, update ↵ | Jim Fehrle | |
| README.rst to match. Bump env_version. | |||
| 2018-09-23 | Documentation for proof diffs | Jim Fehrle | |
| 2018-09-20 | Define flags (binary-valued settings) and tables (settings that are sets) | Jim Fehrle | |
| as separate NotationObject types, include in index. | |||
| 2018-09-20 | [doc] Add another common mistake to the documentation-writing guide | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Add more common mistakes to the documentation-writing guide | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Add a warning about overusing the `coqtop` directive | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Move the LaTeX preamble to a separate .tex file | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix a typo in coqdomain.py | Clément Pit-Claudel | |
| 2018-08-31 | Merge PR #8170: Don't index names starting with `_` in docs | Théo Zimmermann | |
| 2018-08-22 | Fix #8251: remove "the the" occurrences | Gaëtan Gilbert | |
| 2018-07-30 | [sphinx] Use arguments of '.. example::' directive as a title | Clé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-25 | [sphinx] Add a way of skipping names in the indexes. | Théo Zimmermann | |
| 2018-06-19 | [doc] Rewrite and document the prodn directive | Clément Pit-Claudel | |
| It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. | |||
| 2018-05-25 | [doc] Allow more than one signature and name per Sphinx object | Clément Pit-Claudel | |
| As discussed in GH-7556. | |||
| 2018-05-22 | [doc] Document the new report_undocumented_coq_objects setting | Clément Pit-Claudel | |
| 2018-05-22 | [doc] Add a list of common mistakes | Clément Pit-Claudel | |
| 2018-05-15 | [doc] More feedback on doc writer guide | Clément Pit-Claudel | |
| Co-Authored-By: @Zimmi48 | |||
| 2018-05-15 | [doc] Address feedback on doc writer guide | Clément Pit-Claudel | |
| Co-Authored-By: @Zimmi48 | |||
| 2018-05-15 | [doc] Add an ELisp snippet to insert Sphinx roles and quotes | Clément Pit-Claudel | |
| 2018-05-15 | [doc] Add a README to doc/sphinx/ | Clément Pit-Claudel | |
| The readme is auto-generated by combining introductory text with the docstrings in coqdomain.py. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |