aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Collapse)Author
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-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-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
2019-05-22[refman] Add more missing @ signsClément Pit-Claudel
2019-05-21Fixing typos - Part 1JPR
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
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-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-10[User manual] Fix two warnings related to canonical structuresVincent Laporte
2019-05-02Fix #5752: `Hint Mode` ignored for type classes that appear as assumptionsMaxime Dénès
The creation of the local hint db now inherits the union of the modes from the dbs passed to `typeclasses eauto`. We could probably go further and define in a more systematic way the metadata that should be inherited. A lot of this code could also be cleaned-up by defining the merge of databases, so that the search code is parametrized by just one db (the merge of the input ones).
2019-04-30First fixing pass, and experiment with dune-style PR number and author listing.Théo Zimmermann
2019-04-27Minor doc improvement.Théo Zimmermann
2019-04-27[refman] Fix typo.Théo Zimmermann
Noticed by Maxime Dénès.
2019-04-16Update and fix documentation of Program Fixpoint with measureMaxime Dénès
2019-04-10Improve SProp error message to mention the Allow StrictProp flag.Théo Zimmermann
And document the error message.
2019-03-30[Manual] TypoVincent Laporte
2019-03-29typo in ring.rstthery
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Ack-by: pi8027
2019-03-27Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.Jim Fehrle
2019-03-27Deprecate `Refine Instance Mode` optionMaxime Dénès
This is in view of the 8.10 release, after which we will remove the option and the `VtUnknown` classification.
2019-03-26Fix syntax of Typeclasses eauto := in reference manual.Théo Zimmermann
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
This option made the Coercions command follow non-standard scoping rules (effect on `Require` rather than `Import`). It was already marked for deletion in 8.8.
2019-03-18Update doc and changesKazuhiko Sakaguchi
2019-03-18[Manual] Move command Context after Let, and more polishingLysxia
- Refine some `@term` into `@type`
2019-03-17[Manual] Move doc on Let into Section mechanism, and more polishingLysxia
- Put "Section mechanism" example earlier
2019-03-17[Manual] Gather section-specific commands in Section documentation (fix #9704)Lysxia
2019-03-17[Manual] Improve chapter Type classes, and add mention of Context under VariableLysxia
- More consistent code indentation - Nest command variants properly - Make `Context` explanation a bit less terse, with more links - Typesetting bits, add some :cmd: links
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected.
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18Fix doc for Refine Instance ModeGaëtan Gilbert
2019-02-18Fix failing coqtops in type-classes.rstGaëtan Gilbert
2019-02-14[Manual] Fix a referenceVincent Laporte
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
Ack-by: Zimmi48
2019-02-12Fix failing coqtops universe-polymorphism.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
Maybe we should still let it run but let's disable it until we install csdp on the build server at least.
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in extended-pattern-matching.rstGaëtan Gilbert
2019-02-11Small typos in the documentation.Martin Bodin
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
Ack-by: JasonGross Reviewed-by: fajb Reviewed-by: jfehrle
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, ↵Jason Gross
Z.to_euclidean_division_equations
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01. It turns out the 4x was due to .nia.cache (because I didn't clean sufficiently in testing), not due to `subst`.
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
This speeds up the file from 2m32s to ``` real 0m41.851s user 0m41.512s sys 0m0.376s ``` Also note the `subst` trick in the doc.
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
Alas, I have not had time to work on imrpoving the performance of nia, and there has been a request to include this tactic (which is useful on its own) without bundling it into `zify`. So that is what we do here. I leave the definition of it in `PreOmega` in case we want to eventually include it in `zify`/`nia`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:10:29 +0000