aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/ltac.rst
AgeCommit message (Expand)Author
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-06Moving lazymatch and multimatch to simple identifiers.Hugo Herbelin
2020-05-06Mention keywords from g_ltac.mlg used in Ltac.Hugo Herbelin
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-22documentation fixesAntonio Nikishaev
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-22[refman] Add more missing @ signsClément Pit-Claudel
2019-05-22[refman] Misc fixes (mostly missing '@' signs)Clément Pit-Claudel
2019-05-21Fixing typos - Part 1JPR
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-10Better title for the first example of the Ltac examples section.Théo Zimmermann
2019-05-09Improve the first two Ltac examples.Théo Zimmermann
2019-05-09Rewording, language improvements.Théo Zimmermann
2019-05-08[refman] Move all the Ltac examples to the Ltac chapter.Théo Zimmermann
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
2019-03-27[doc] [abstract] Document a bit some problems with abstract.Emilio Jesus Gallego Arias
2019-03-08[sphinx] Fix typo in local application of tacticshawnzug
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 15:30:25 +0000