aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2018-07-29Documenting custom entries in the reference manual + CHANGES.Hugo Herbelin
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error me...Hugo Herbelin
2018-07-28Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical Structu...Théo Zimmermann
2018-07-28Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to un...Théo Zimmermann
2018-07-27Missing backslash in the documentation file.Martin Bodin
2018-07-26[sphinx] Do name cleanup in handle_signatureClément Pit-Claudel
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the Refe...Zeimer
2018-07-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
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-23Add test for repeated section with same nameJasper Hugunin
2018-07-22Docs: minor typo in "Template Polymorphism"Timothy Bourke
2018-07-22Docs: minor typo in W-Ind relative to textTimothy Bourke
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-21Docs: Fix p values in CIC Inductive Defs examplesTimothy Bourke
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-19Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' o...Zeimer
2018-07-19Fixed some typos and grammar errors from section 'The language' of the Refere...Zeimer
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-13Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of th...Théo Zimmermann
2018-07-12Fixed typos, wording and grammar errors in the Preamble of the Reference Manu...Zeimer
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-10fixed typo for assert_suceedcharguer
2018-07-10Merge PR #8028: Fix a few typosThéo Zimmermann
2018-07-10Merge PR #8025: Fix rst syntax for `quote ident {ident}`Théo Zimmermann
2018-07-10Fix typo in doc/proof-engine/tactics.rst.whitequark
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-09Fix rst syntax for `quote ident {ident}`Joachim Breitner
2018-07-08Remove Emacs modes.Théo Zimmermann
2018-07-07Merge PR #7921: Archive the `gallina` toolMaxime Dénès
2018-07-04doc: Fix markup in Calculus of Inductive ConstructionsFabian
2018-07-03Describe attributes in the documentation.Vincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsThéo Zimmermann
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-01Document option Uniform Inductive ParametersJasper Hugunin
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
2018-06-29doc: Fix typesetting in Gallina extensionsLysxia
2018-06-28Self-credit for the work done.Théo Zimmermann
2018-06-28wrong sphinx syntaxAmbroise
2018-06-28Update gallina-extensions.rstAmbroise
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:32:42 +0000