aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2019-06-03Update tutorial plugin to use sigma, in keeping with doc recommendationsTalia Ringer
2019-06-03Update doc to reflect that PG now supports Coq-generated proof diffsJim Fehrle
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
This feature makes it possible to tell type inference to type applications of a global `foo` using typing information from the context once the `n` first arguments are known. The syntax is: `Arguments foo x y | z`. Closes #7910
2019-05-26Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter.Enrico Tassi
Reviewed-by: gares
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
To prevent confusion, forbidding a mix of the "injection term as pat1 ... patn" and of the "injection term as [= pat1 ... patn]" syntax: If a "[= ...]" occurs, this should be a singleton list of patterns.
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
We simply pass them as arguments, now that they are not called by the kernel anymore. The checker definitely needs to access the opaque proofs. In order not to touch the API at all, I added a hook there, but it could also be provided as an additional argument, at the cost of changing all the upwards callers.
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-23Use new coqrst syntax for alternatives in SSReflect chapter.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 19:46:18 +0000