aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
2019-05-23Merge PR #10192: More miscellaneous refman fixes (reopened version of #10187)Théo Zimmermann
Ack-by: Zimmi48
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl
2019-05-22[refman] Add more missing @ signsClément Pit-Claudel
2019-05-22[refman] Misc fixes (mostly missing '@' signs)Clément Pit-Claudel
Co-Authored-By: @Zimmi48
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
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: gares Reviewed-by: jfehrle Reviewed-by: vbgl
2019-05-22Merge PR #10178: Improve doc for generalizing bindersThéo Zimmermann
Reviewed-by: Zimmi48
2019-05-22Improve doc for generalizing bindersGaëtan Gilbert
2019-05-21Fixing typos - Part 1JPR
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
This lets us avoid passing ~ontop to do_definition and co, and after #10050 to even more functions.
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
It's used a few times in the stdlib (a couple of which need no other change when removing the !) and not at all throughout our CI. Considering that I think it's fair enough to remove it.
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
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
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
notations Reviewed-by: Zimmi48 Ack-by: jfehrle
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
Closes GH-8482.
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
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: jfehrle Reviewed-by: vbgl
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵Enrico Tassi
prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: jashug
2019-05-13Merge PR #10079: [refman] Move Ltac examples to Ltac chapter.Vincent Laporte
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
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
+ adding a go-to-end binding + improving documentation Reviewed-by: gares Ack-by: herbelin Reviewed-by: ppedrot
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
Attributes that enable/disable a feature can have an explicit value (default is enable when the attribute is present). Three-valued boolean attributes do not support this: what would `#[local(false)]` mean?
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
Reviewed-by: cpitclaudel Reviewed-by: vbgl
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
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-05-08[refman] Move all the Ltac examples to the Ltac chapter.Théo Zimmermann
The Detailed examples of tactics chapter can be removed when the remaining examples are moved closer to the definitions of the corresponding tactics. This commit also moves back the footnotes from the Tactics chapter at the end of the chapter, and removes an old footnote that doesn't matter anymore.
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
Use it to not include unreleased changes when building a released version.
2019-05-07Added "Recursively" for the R optionRobert Rand
2019-05-07Added description of QRobert Rand
Note that this description is identical to that of R. R should maybe start with the word "Recursively"?
2019-05-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ↵Clément Pit-Claudel
database. Reviewed-by: cpitclaudel
2019-05-07Define minimum Sphinx version in conf.py.Théo Zimmermann
We set the minimum Sphinx version in conf.py to the one that we test in our CI and the one that is documented in doc/README.md. Hopefully, it will allow users with lower Sphinx verisons get better error messages.
2019-05-07Merge PR #10053: Document change_no_check variantsThéo Zimmermann
Ack-by: JasonGross Reviewed-by: Zimmi48
2019-05-07Merge PR #10002: Integrate ltac2Théo Zimmermann
Ack-by: JasonGross Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: jfehrle Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-05-07[refman] Add a note reminding about the typeclass_instances database.Théo Zimmermann
Closes #10072.
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions.
2019-05-05Add changelog entry about moving changelog to refman.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 00:11:53 +0000