aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proofs/automatic-tactics/auto.rst
AgeCommit message (Collapse)Author
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-01-21Improve wording for #13384Jim Fehrle
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-16Document the new warning.Pierre-Marie Pédrot
2020-11-16Tentative fix for the refman.Pierre-Marie Pédrot
2020-11-15Document the new export locality for the remaining hint commands.Pierre-Marie Pédrot
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-05Add new sections to automatic tactic chapter.Théo Zimmermann
2020-11-05Keep only content about auto.Théo Zimmermann
2020-11-05Move some content to a new page on automation.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 03:40:32 +0000