aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/ltac.rst
AgeCommit message (Expand)Author
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-05Documenting the Ltac Backtrace flag.Pierre-Marie Pédrot
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
2019-01-23Fix the information of the level of ; vs ; [ ]Théo Zimmermann
2019-01-23Improve the note in the beginning of the Ltac chapter.Théo Zimmermann
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-17Add missing index entries.Théo Zimmermann
2018-09-12Manual: fix documentation of the “fresh” tacticVincent Laporte
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-16Merge PR #8109: [doc] Fix grammar of goal selectors.Maxime Dénès
2018-07-21[doc] Fix grammar of goal selectors.Théo Zimmermann
2018-07-21A few Sphinx fixes in the Ltac chapter.Théo Zimmermann
2018-07-20Small improvements suggested in comments to PR #8086.Zeimer
2018-07-20Improved chapter 'The tactic language' of the Reference Manual.Zeimer
2018-07-10fixed typo for assert_suceedcharguer
2018-05-25[doc] Allow more than one signature and name per Sphinx objectClément Pit-Claudel
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-05[sphinx] Add indices for only, all and par.Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
2018-05-05[sphinx] Replace remaining `@natural` by `@num`.Théo Zimmermann
2018-05-05[sphinx] Use references for command Info.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05Clean-up around options.Théo Zimmermann
2018-05-05[sphinx] Fix some references.Théo Zimmermann
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14[Sphinx] Add chapter 9.Théo Zimmermann
2018-04-14[Sphinx] Move chapter 9 to new infrastructure.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:42:35 +0000