aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Expand)Author
2018-08-28Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter.Clément Pit-Claudel
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-24Merge PR #8266: Minor Sphinx improvements in the bullet documentation.Clément Pit-Claudel
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-22Add missing spaces.Théo Zimmermann
2018-08-22[sphinx] Improve Case analysis and induction section.Théo Zimmermann
2018-08-22[refman] Fixing two nested lemma errors.Théo Zimmermann
2018-08-22[sphinx] Fixing of the beginning of the Tactics chapter.Théo Zimmermann
2018-08-17Define bullet production token.Théo Zimmermann
2018-08-17Minor Sphinx improvements in the bullet documentation.Théo Zimmermann
2018-08-16Merge PR #8109: [doc] Fix grammar of goal selectors.Maxime Dénès
2018-08-16Merge PR #8108: A few Sphinx fixes in the Ltac chapter.Maxime Dénès
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error me...Hugo Herbelin
2018-07-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
2018-07-24Update the documentation w.r.t. the new error raised by unify.Pierre-Marie Pédrot
2018-07-21Solved problems with snippets giving errors in chapter 'Detailed examples of ...Zeimer
2018-07-21Rewrote examples about permutations, logic and type isomorphisms: changed the...Zeimer
2018-07-21Improvements for the chapter 'Detailed examples of tactics' of the Reference ...Zeimer
2018-07-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' an...Théo Zimmermann
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-20Added :undocumented: and :cmd: as suggested in comments for PR #8072.Zeimer
2018-07-20Fixed many spelling and grammar errors in the chapters 'Vernacular commands',...Zeimer
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-10fixed typo for assert_suceedcharguer
2018-07-10Merge PR #8028: Fix a few typosThéo Zimmermann
2018-07-10Fix typo in doc/proof-engine/tactics.rst.whitequark
2018-07-09Fix rst syntax for `quote ident {ident}`Joachim Breitner
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-06-22[ssr] document {}/viewEnrico Tassi
2018-06-22[ssr] document rewrite {}fooEnrico Tassi
2018-06-21Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.Maxime Dénès
2018-06-19Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Pierre-Marie Pédrot
2018-06-19[doc] Fix a typo in the ssreflect chapterClément Pit-Claudel
2018-06-19[doc] Fix uncaught duplicate-label errors in the SSReflect chapterClément Pit-Claudel
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-18Fix #7829: Spurious documentation failures.Théo Zimmermann
2018-06-05Improve links to SSR tactics, and some other improvements.Théo Zimmermann
2018-06-05Workaround a weird error of .. coqtop::Théo Zimmermann
2018-06-05Remove many abusive .. coqtop in SSR chapter.Théo Zimmermann
2018-06-05A few additional small fixes.Théo Zimmermann
2018-06-05[sphinx] Fix missing indices warnings.Théo Zimmermann
2018-06-05[ssr] index entry for "without loss", "suffices" and "generally have"Enrico Tassi
2018-06-05[ssr] some fixes to the documentation markupEnrico Tassi
2018-06-05[sphinx] Start fixing SSR chapter.Théo Zimmermann
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7601: Fix notation for code snippet in documentationMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 22:43:20 +0000