| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-09-11 | [refman] Rename num to natural | Pierre Roux | |
| 2020-08-25 | Require NsatzTactic: nsatz support for Z and Q | Jason Gross | |
| The purpose of `NsatzTactic` is to allow using `nsatz` without the dependency on real axioms. So we declare the instances for `Z` and `Q` in that file, so that users don't have to re-create them. Fixes #12860 | |||
| 2018-12-03 | Closes #9118: single backticks are made equivalent to double backticks; try ↵ | Théo Zimmermann | |
| to fix all misuses. | |||
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-08-01 | Added a tactic index entry for nsatz, reformatted commands in chapter ↵ | Zeimer | |
| 'Generalized Rewriting' and renamed the chapter Nsatz from _nsatz to _nsatz_chapter. | |||
| 2018-08-01 | Improved grammar and spelling in the remaining chapters of the Reference Manual. | Zeimer | |
| 2018-04-14 | [sphinx] Fix many warnings. | Théo Zimmermann | |
| Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | |||
| 2018-03-29 | [Sphinx] Add chapter 26 | Maxime Dénès | |
| Thanks to Paul Steckler for porting this chapter. | |||
| 2018-03-29 | [Sphinx] Move chapter 26 to new infrastructure | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |