| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-07-22 | Merge PR #10441: Attach the universe polymorphic status to sections. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: mattam82 | |||
| 2019-07-18 | [doc] Fix typo in doc/sphinx/addendum/ring.rst | Wojciech Nawrocki | |
| 2019-07-18 | Adding changelog and documentation. | Pierre-Marie Pédrot | |
| 2019-07-05 | Correct doc about default value for Typeclasses Dependency Order | Gaëtan Gilbert | |
| 2019-07-02 | Improve the ambiguous paths warning to indicate which path is ambiguous with ↵ | Kazuhiko Sakaguchi | |
| new one | |||
| 2019-06-04 | [rewrite] Add Morphism syntax made different for module type parameters | Enrico Tassi | |
| 2019-05-24 | Merge 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-23 | do 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-23 | Define 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 @ signs | Clément Pit-Claudel | |
| 2019-05-21 | Fixing typos - Part 1 | JPR | |
| 2019-05-20 | Remove Refine Instance Mode option | Maxime Dénès | |
| 2019-05-19 | [refman] Fix up the documentation of Instance and Existing Instance | Clément Pit-Claudel | |
| 2019-05-19 | [refman] Misc fixes (indentation, whitespace, notation syntax) | Clément Pit-Claudel | |
| 2019-05-19 | Merge 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 notations | Clément Pit-Claudel | |
| Closes GH-8482. | |||
| 2019-05-10 | [Attributes] Allow explicit value for two-valued attributes | Vincent 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 structures | Vincent Laporte | |
| 2019-05-02 | Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions | Maxime 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-30 | First fixing pass, and experiment with dune-style PR number and author listing. | Théo Zimmermann | |
| 2019-04-27 | Minor doc improvement. | Théo Zimmermann | |
| 2019-04-27 | [refman] Fix typo. | Théo Zimmermann | |
| Noticed by Maxime Dénès. | |||
| 2019-04-16 | Update and fix documentation of Program Fixpoint with measure | Maxime Dénès | |
| 2019-04-10 | Improve SProp error message to mention the Allow StrictProp flag. | Théo Zimmermann | |
| And document the error message. | |||
| 2019-03-30 | [Manual] Typo | Vincent Laporte | |
| 2019-03-29 | typo in ring.rst | thery | |
| 2019-03-28 | Merge PR #9743: Relax the ambiguous path condition of coercion | Enrico Tassi | |
| Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Ack-by: pi8027 | |||
| 2019-03-27 | Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual. | Jim Fehrle | |
| 2019-03-27 | Deprecate `Refine Instance Mode` option | Maxime 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-26 | Fix syntax of Typeclasses eauto := in reference manual. | Théo Zimmermann | |
| 2019-03-25 | Remove `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-18 | Update doc and changes | Kazuhiko Sakaguchi | |
| 2019-03-18 | [Manual] Move command Context after Let, and more polishing | Lysxia | |
| - Refine some `@term` into `@type` | |||
| 2019-03-17 | [Manual] Move doc on Let into Section mechanism, and more polishing | Lysxia | |
| - 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 Variable | Lysxia | |
| - 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-14 | Documentation for SProp | Gaë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-18 | Using options abort and restart of coqtop directive in the manual. | Théo Zimmermann | |
| 2019-02-18 | Fix doc for Refine Instance Mode | Gaëtan Gilbert | |
| 2019-02-18 | Fix failing coqtops in type-classes.rst | Gaëtan Gilbert | |
| 2019-02-14 | [Manual] Fix a reference | Vincent Laporte | |
| 2019-02-13 | Merge PR #9553: Sphinx various fixing of failing commands | Théo Zimmermann | |
| Ack-by: Zimmi48 | |||
| 2019-02-12 | Fix failing coqtops universe-polymorphism.rst | Gaëtan Gilbert | |
| 2019-02-12 | Fix failing coqtops in ring.rst | Gaëtan Gilbert | |
| 2019-02-12 | Fix 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-12 | Fix failing coqtops in generalized-rewriting.rst | Gaëtan Gilbert | |
| 2019-02-12 | Fix failing coqtops in extended-pattern-matching.rst | Gaëtan Gilbert | |
| 2019-02-11 | Small typos in the documentation. | Martin Bodin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |