aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/proof-engine/tactics.rst
Commit message (Expand)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
* Added :undocumented: and :cmd: as suggested in comments for PR #8072.Gravatar Zeimer2018-07-20
* Fixed many spelling and grammar errors in the chapters 'Vernacular commands',...Gravatar Zeimer2018-07-20
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
* Merge PR #8028: Fix a few typosGravatar Théo Zimmermann2018-07-10
|\
| * Fix typo in doc/proof-engine/tactics.rst.Gravatar whitequark2018-07-10
* | Fix rst syntax for `quote ident {ident}`Gravatar Joachim Breitner2018-07-09
|/
* hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
* Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
* A few additional small fixes.Gravatar Théo Zimmermann2018-06-05
* Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\
* \ Merge PR #7601: Fix notation for code snippet in documentationGravatar Maxime Dénès2018-06-04
|\ \
| | * Documenting the deprecation.Gravatar Pierre-Marie Pédrot2018-06-04
| |/ |/|
* | Merge two clearbody docsGravatar Théo Winterhalter2018-06-01
* | Indicate in the doc that clearbody can take several identsGravatar Théo Winterhalter2018-05-31
| * Fix notation for code snippet in documentationGravatar Anton Trunov2018-05-25
|/
* [sphinx] Fix mistake in index.Gravatar Théo Zimmermann2018-05-16
* [sphinx] Improve rewrite section in tactic chapter.Gravatar Théo Zimmermann2018-05-16
* [doc] Small fixesGravatar Clément Pit-Claudel2018-05-15
* Merge PR #7374: [sphinx] More fatal warnings.Gravatar Maxime Dénès2018-05-14
|\
* | Doc: Renaming an old-style numerical evar in an alphabetical one.Gravatar Hugo Herbelin2018-05-11
* | Doc: Moving `\forall` to `forall` in file tactics.rst.Gravatar Hugo Herbelin2018-05-11
* | Doc: Some quotes missing in file tactics.rst.Gravatar Hugo Herbelin2018-05-11
* | Replacing a broken reference by hyperlinks in chapter tactics.Gravatar Hugo Herbelin2018-05-11
* | A few fixes in chapter tactics.Gravatar Hugo Herbelin2018-05-11
| * [sphinx] Fix new warnings related to tacn, cmd, opt...Gravatar Théo Zimmermann2018-05-09
| * Replacing a broken reference by hyperlinks in chapter tactics.Gravatar Hugo Herbelin2018-05-09
| * A few fixes in chapter tactics.Gravatar Hugo Herbelin2018-05-09
|/
* [sphinx] Fixes around apply, including indentation and fixing a Coq warning.Gravatar Théo Zimmermann2018-05-05
* [sphinx] Fixes around refine, including indentation and a hard-coded ref.Gravatar Théo Zimmermann2018-05-05
* [sphinx] Improvements around injection tactic.Gravatar Théo Zimmermann2018-05-05
* [sphinx] Improve part about Hints.Gravatar Théo Zimmermann2018-05-05
* Clean-up around cmd documentation.Gravatar Théo Zimmermann2018-05-05
* [sphinx] More reference fixes.Gravatar Théo Zimmermann2018-05-05
* Fix error messages and make them consistent.Gravatar Théo Zimmermann2018-05-05
* Add direct reference to congruence with.Gravatar Théo Zimmermann2018-05-05
* Clean-up around options.Gravatar Théo Zimmermann2018-05-05
* debug trivial and debug auto were not in the tactic index.Gravatar Théo Zimmermann2018-05-05
* [sphinx] Backport reformulation.Gravatar Théo Zimmermann2018-05-05
* Make "intro"/"intros" progress on existential variables.Gravatar Hugo Herbelin2018-05-02
* Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
* [Sphinx] Clean-up indicesGravatar Maxime Dénès2018-04-16
* [Sphinx] Fix a lot of references and description of optionsGravatar Maxime Dénès2018-04-16
* [Sphinx] Fix all remaining warnings.Gravatar Maxime Dénès2018-04-14
* [sphinx] Fix many warnings.Gravatar Théo Zimmermann2018-04-14
* Clarify wording in tactics documentation.Gravatar Théo Zimmermann2018-03-25
* [Sphinx] Add chapter 8Gravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 8 to new infrastructureGravatar Maxime Dénès2018-03-15