aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2019-05-23Merge PR #10118: Make progress toward #9411: reject new undefined references.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-05-24Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ggonthier Reviewed-by: herbelin Ack-by: jfehrle Reviewed-by: mattam82
2019-05-23Make progress toward #9411: reject new undefined references.Théo Zimmermann
We list preexisting undefined tokens explicitly in `doc/sphinx/conf.py` and prevent new ones from being introduced by making it a fatal warning. This list should be seen as a TODO. Once it is emptied, #9411 can be closed.
2019-05-23Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2019-05-23Merge PR #10217: Less undefined tokensClément Pit-Claudel
Ack-by: JasonGross Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns, rather than infix `|`, making pattern syntax consistent with term syntax. * disable extending `pattern` grammar with notation incompatible with the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p | q)` divisibility notation used by `Numbers`. * emit a (disabled by default) `disj-pattern-notation` warning when such `Notation` is attempted. * update documentation accordingly; document incompatibilities in `changelog`. * comment special treatment of `(num)` in grammar. * update file extensions in `Pcoq` header comment. * correct the keyword declarations to reflect the contents of the grammar files; perhaps there should be an option to disable implicit keyword extension in a `.mlg` file, so that these lists could actually be checked. * parse the `|}` manifest record terminator as `|` followed by `}`, eliminating the `|}` token which conflicts with notations that use `|` as a terminator (such as, absolute value, norm, or cardinal in MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator, `bar_cbrace` rule checks for contiguous symbols, this change entails no visible behaviour change.
2019-05-23Suggestions from review.Théo Zimmermann
Co-authored-by: Jason Gross <jgross@mit.edu>
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
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
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
2019-05-23Update `Bind Scope` documentation to reflect ↵Maxime Dénès
3d09e39dd423d81c6af3e991d5b282ea8608646b The commit mentioned above changed the semantics of `Bind Scope` to a dynamic binding behavior. It forgot to update the documentation. Fixes #10064
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-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
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-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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 07:59:15 +0000