aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Documenting "Declare Scope".Hugo Herbelin
2018-09-10Merge PR #8104: Warnings on coercions used without being ImportedEnrico Tassi
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-07Recover lost snippetMatěj G
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-09-04Merge PR #7684: [doc] Build ML API documentation artifact.Gaëtan Gilbert
2018-09-03[doc] Build ML API documentation artifact.Emilio Jesus Gallego Arias
2018-08-31Give a proper error message on num-not in functorJason Gross
2018-08-31[numeral notations] support aliasesJason Gross
2018-08-31Add periods in response to PR commentsJason Gross
2018-08-31Add a warning about abstract after being a no-opJason Gross
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
2018-08-31Numeral Notation: minor text improvements suggested by J. GrossPierre Letouzey
2018-08-31Numeral Notation: some documentation in the refmanPierre Letouzey
2018-08-31Numeral Notation for natPierre Letouzey
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-30Merge PR #8292: Create SPHINXWARNERROR variable to control Sphinx "warn as er...Théo Zimmermann
2018-08-29Merge PR #8353: [sphinx] Fix timeout issue by splitting imports.Clément Pit-Claudel
2018-08-29Merge PR #8345: Add index for focusing braces.Clément Pit-Claudel
2018-08-29Create SPHINXWARNERROR variable that controls whether the SphinxJim Fehrle
2018-08-29[sphinx] Fix timeout issue by splitting imports.Théo Zimmermann
2018-08-28Merge PR #8334: Fix a casing problem noticed by Lars Dölle on Coq-Club.Clément Pit-Claudel
2018-08-28Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter.Clément Pit-Claudel
2018-08-28Merge PR #8281: Trivial Sphinx fix in doc.Clément Pit-Claudel
2018-08-28Add index for focusing braces.Théo Zimmermann
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-27Fix a casing problem noticed by Lars Dölle on Coq-Club.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-21Trivial Sphinx fix in doc.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 #8198: Fix broken link.Maxime Dénès
2018-08-16Merge PR #8111: Docs: Fix p values in CIC Inductive Defs examplesMaxime Dénès
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-08-06Merge PR #8189: Some trivial fixes to the custom entry documentation.Emilio Jesus Gallego Arias
2018-08-04Merge PR #8142: Improved the grammar and spelling of chapter 'Syntax extensio...Théo Zimmermann
2018-08-04Improved the grammar and spelling of chapter 'Syntax extensions and interpret...Zeimer
2018-08-03Fix docs on arguments to setoid_replace. Fixes #8213Langston Barrett
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 11:55:28 +0000