aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
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-21Remove definition-not-visible warningGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
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] Raise an error when a notation doesn't parseClément Pit-Claudel
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-10Changelog for PR #10076Vincent 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-08Update release process documentation and changelog entry.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
2019-05-07[refman] Add a note reminding about the typeclass_instances database.Théo Zimmermann
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
2019-05-05Add changelog entry about moving changelog to refman.Théo Zimmermann
2019-05-05Create categories in changelog.Théo Zimmermann
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
2019-05-04Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear a...Pierre-Marie Pédrot
2019-05-03Copy-editing from code reviewJason Gross
2019-05-03Documentation for change_no_check untested variantsPaolo G. Giarrusso
2019-05-03Document _no_check tactics (#3225)Paolo G. Giarrusso
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 13:11:16 +0000