aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Suggestions from review.Théo Zimmermann
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23More misc refman fixes, less undefined tokens.Théo Zimmermann
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-23Use new coqrst syntax for alternatives in SSReflect chapter.Théo Zimmermann
2019-05-23Update `Bind Scope` documentation to reflect 3d09e39dd423d81c6af3e991d5b282ea...Maxime Dénès
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-22[refman] Give explicit names to the various 'Arguments' commandsClément Pit-Claudel
2019-05-22Merge PR #10203: Fixing typos - Part 1Théo Zimmermann
2019-05-22Merge PR #10178: Improve doc for generalizing bindersThéo Zimmermann
2019-05-22Ltac2 doc fix: syntax for extending an open variant type.Théo Zimmermann
2019-05-22Improve doc for generalizing bindersGaëtan Gilbert
2019-05-21Fixing typos - Part 1JPR
2019-05-20Minor Ltac2 documentation fix: type parameters are optional.Théo Zimmermann
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-19[refman] Document etransitivityClément Pit-Claudel
2019-05-19[refman] Fix up the grammar entry for field_defClément Pit-Claudel
2019-05-19[refman] Add a .. cmd:: header for Reserved Notation and Reserved InfixClément Pit-Claudel
2019-05-19[refman] Fix up the documentation of Instance and Existing InstanceClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-19Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ...Théo Zimmermann
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
2019-05-13Missing change entry for #9854.Théo Zimmermann
2019-05-13Move last changelog entries for 8.10+beta1.Théo Zimmermann
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
2019-05-13Merge PR #10079: [refman] Move Ltac examples to Ltac chapter.Vincent Laporte
2019-05-12[refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'Clément Pit-Claudel
2019-05-11Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS ...Pierre-Marie Pédrot
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[refman] Mention the `#[canonical(false)]` attributeVincent Laporte
2019-05-10[Attributes] Allow explicit value for two-valued attributesVincent Laporte
2019-05-10[User manual] Fix two warnings related to canonical structuresVincent Laporte
2019-05-10Merge PR #10080: Define minimum Sphinx version in conf.py.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-08Define a new `is_a_released_version` variable in configure.ml.Théo Zimmermann
2019-05-07Added "Recursively" for the R optionRobert Rand
2019-05-07Added description of QRobert Rand
2019-05-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ...Clément Pit-Claudel
2019-05-07Define minimum Sphinx version in conf.py.Théo Zimmermann
2019-05-07Merge PR #10053: Document change_no_check variantsThéo Zimmermann
2019-05-07Merge PR #10002: Integrate ltac2Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 23:08:55 +0000