aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/tactics.rst
AgeCommit message (Expand)Author
2018-05-05[sphinx] Fixes around apply, including indentation and fixing a Coq warning.Théo Zimmermann
2018-05-05[sphinx] Fixes around refine, including indentation and a hard-coded ref.Théo Zimmermann
2018-05-05[sphinx] Improvements around injection tactic.Théo Zimmermann
2018-05-05[sphinx] Improve part about Hints.Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
2018-05-05[sphinx] More reference fixes.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05Add direct reference to congruence with.Théo Zimmermann
2018-05-05Clean-up around options.Théo Zimmermann
2018-05-05debug trivial and debug auto were not in the tactic index.Théo Zimmermann
2018-05-05[sphinx] Backport reformulation.Théo Zimmermann
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-16[Sphinx] Fix a lot of references and description of optionsMaxime Dénès
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14[sphinx] Fix many warnings.Théo Zimmermann
2018-03-25Clarify wording in tactics documentation.Théo Zimmermann
2018-03-15[Sphinx] Add chapter 8Maxime Dénès
2018-03-15[Sphinx] Move chapter 8 to new infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 09:06:23 +0000