| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle | |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-11-10 | Convert logic.rst 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-11-09 | Remove virtually unused replace rule. | Théo Zimmermann | |
| 2020-11-05 | Change the title of the automatic tactic chapter and of its sections. | Théo Zimmermann | |
| Prefer the term 'solver' to 'decision procedure'. | |||
| 2020-10-24 | Convert misc chapters to prodn | Jim Fehrle | |
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann | |
| 2020-10-02 | {new,setoid_}ring -> ring | Maxime Dénès | |
| I believe this renaming makes it easier for new contributors to discover the code of `ring`. | |||
| 2020-06-08 | Convert Ltac chapter to prodn | Jim Fehrle | |
| 2020-06-08 | Make automatic name generation for directives more consistent: | Jim Fehrle | |
| - by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except - don't generate a name for cmdv and tacv - generate more flexibily for exn, warn and attr | |||
| 2020-03-26 | Shrink refman-prelude files. | Théo Zimmermann | |
| 2020-03-09 | Remove some productionlists | Jim Fehrle | |
| 2019-07-18 | [doc] Fix typo in doc/sphinx/addendum/ring.rst | Wojciech Nawrocki | |
| 2019-05-23 | Define many undefined tokens, and other misc fixes. | Théo Zimmermann | |
| Progress towards #9411, extracted from #10118, rebased ontop of #10192. | |||
| 2019-03-29 | typo in ring.rst | thery | |
| 2019-02-12 | Fix failing coqtops in ring.rst | Gaëtan Gilbert | |
| 2019-01-22 | Remove unneeded | in productionlists | Jim Fehrle | |
| 2018-12-03 | Closes #9118: single backticks are made equivalent to double backticks; try ↵ | Théo Zimmermann | |
| to fix all misuses. | |||
| 2018-11-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-08-31 | Uniformized 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-07-29 | Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring ↵ | Zeimer | |
| and field' chapters of the Reference Manual. | |||
| 2018-06-19 | [doc] Use productionlist instead of prodn in ring.rst | Clément Pit-Claudel | |
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | Fix error messages and make them consistent. | Théo Zimmermann | |
| All the error messages start with a capitalized letter and end with a dot. | |||
| 2018-04-14 | [Sphinx] Fix all remaining warnings. | Maxime Dénès | |
| 2018-03-30 | [Sphinx] Add chapter 25 | Maxime Dénès | |
| Thanks to Laurent Théry for porting this chapter. | |||
| 2018-03-30 | [Sphinx] Move chapter 25 to new infrastructure | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |