aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Expand)Author
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
2019-02-14Document the now_show tactic.Théo Zimmermann
2019-02-14[Manual] Clean examples for `apply`Vincent Laporte
2019-02-14[Manual] Don’t use `Undo` in ssreflect examplesVincent Laporte
2019-02-14[Manual] Clean examples about `inversion` tacticVincent Laporte
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
2019-02-12Fix failing coqtops in tactics.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ssreflect-proof-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-12Improve the documentation of auto.Théo Zimmermann
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2019-02-05Documenting the Ltac Backtrace flag.Pierre-Marie Pédrot
2019-02-05Add advice and an example to the documentation of fold.Théo Zimmermann
2019-01-28Surround "assumption" with :tacn:`` in tactics.rstRyan Scott
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
2019-01-24[doc] warn that (automatic) clears can result in errorsEnrico Tassi
2019-01-24[doc] more precise description of when automatic clears are triggeredEnrico Tassi
2019-01-24[doc] explain how to avoid automatic clearsEnrico Tassi
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
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
2019-01-22clarify when an ident is added to the clear switchEnrico Tassi
2019-01-22Apply suggestions from code reviewThéo Zimmermann
2019-01-21ring and field simplify can take no argumentsthery
2019-01-21[ssr] better structure the ipats docEnrico Tassi
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2018-12-19[doc] typoEnrico Tassi
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-12-14Fix the SSReflect chapter regarding objects without bodies.Théo Zimmermann
2018-12-11Add missing formatting.Théo Zimmermann
2018-12-11Document the deprecation of hint declaration withou database in refman.Théo Zimmermann
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-06Improve rendering of the credits.Guillaume Melquiond
2018-10-24[Manual] Prevent an irrelevant warning to show upVincent Laporte
2018-10-24[Manual] Avoid using deprecated “Focus”Vincent Laporte
2018-10-24[Manual] Fix rendering of an exampleVincent Laporte
2018-10-24[Manual] TypoVincent Laporte
2018-10-24[Manual] Fix an exampleVincent Laporte
2018-10-24[Manual] Fix layout of a listVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 05:50:00 +0000