aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
This allows to refer to them from other part of the manual without any ambiguity.
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
Reviewed-by: Zimmi48
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
From the CHANGES file in branch v8.9.
2019-06-12Merge PR #10310: Fix #10283: clearer dependency documentation for building ↵Clément Pit-Claudel
CoqIDE. Reviewed-by: cpitclaudel Reviewed-by: ejgallego
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic ↵Théo Zimmermann
definitions Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ggonthier Reviewed-by: herbelin
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the ↵Emilio Jesus Gallego Arias
vernac syntax Reviewed-by: cpitclaudel Reviewed-by: ejgallego Ack-by: herbelin
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
Slight improving of style in passing.
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-06-03Merge PR #10261: Update doc to reflect that PG now supports Coq-generated ↵Théo Zimmermann
proof diffs Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel Ack-by: erikmd
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 14:36:15 +0000