| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-11 | Merge 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-10 | Use Print Custom Grammar to inspect custom entries | Jasper Hugunin | |
| 2019-05-10 | [refman] Mention the `#[canonical(false)]` attribute | Vincent Laporte | |
| 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 | Changelog for PR #10076 | Vincent Laporte | |
| 2019-05-10 | [User manual] Fix two warnings related to canonical structures | Vincent Laporte | |
| 2019-05-10 | Merge PR #10080: Define minimum Sphinx version in conf.py. | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel Reviewed-by: vbgl | |||
| 2019-05-10 | Better title for the first example of the Ltac examples section. | Théo Zimmermann | |
| 2019-05-09 | Improve the first two Ltac examples. | Théo Zimmermann | |
| 2019-05-09 | Rewording, language improvements. | Théo Zimmermann | |
| Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2019-05-08 | [refman] Move all the Ltac examples to the Ltac chapter. | Théo Zimmermann | |
| The Detailed examples of tactics chapter can be removed when the remaining examples are moved closer to the definitions of the corresponding tactics. This commit also moves back the footnotes from the Tactics chapter at the end of the chapter, and removes an old footnote that doesn't matter anymore. | |||
| 2019-05-08 | Update release process documentation and changelog entry. | Théo Zimmermann | |
| 2019-05-08 | Define a new `is_a_released_version` variable in configure.ml. | Théo Zimmermann | |
| Use it to not include unreleased changes when building a released version. | |||
| 2019-05-07 | Added "Recursively" for the R option | Robert Rand | |
| 2019-05-07 | Added description of Q | Robert Rand | |
| Note that this description is identical to that of R. R should maybe start with the word "Recursively"? | |||
| 2019-05-07 | Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ↵ | Clément Pit-Claudel | |
| database. Reviewed-by: cpitclaudel | |||
| 2019-05-07 | Define minimum Sphinx version in conf.py. | Théo Zimmermann | |
| We set the minimum Sphinx version in conf.py to the one that we test in our CI and the one that is documented in doc/README.md. Hopefully, it will allow users with lower Sphinx verisons get better error messages. | |||
| 2019-05-07 | Merge PR #10053: Document change_no_check variants | Théo Zimmermann | |
| Ack-by: JasonGross Reviewed-by: Zimmi48 | |||
| 2019-05-07 | Merge PR #10002: Integrate ltac2 | Théo Zimmermann | |
| Ack-by: JasonGross Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: jfehrle Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2019-05-07 | [refman] Add a note reminding about the typeclass_instances database. | Théo Zimmermann | |
| Closes #10072. | |||
| 2019-05-07 | Integrate build and documentation of Ltac2 | Maxime Dénès | |
| Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions. | |||
| 2019-05-05 | Add changelog entry about moving changelog to refman. | Théo Zimmermann | |
| 2019-05-05 | Create categories in changelog. | Théo Zimmermann | |
| 2019-05-05 | New infrastructure for the unreleased changelog. | Théo Zimmermann | |
| Move existing entries. | |||
| 2019-05-04 | Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear ↵ | Pierre-Marie Pédrot | |
| as assumptions Ack-by: RalfJung Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: maximedenes Reviewed-by: ppedrot Ack-by: robbertkrebbers | |||
| 2019-05-03 | Copy-editing from code review | Jason Gross | |
| Co-Authored-By: Blaisorblade <p.giarrusso@gmail.com> | |||
| 2019-05-03 | Documentation for change_no_check untested variants | Paolo G. Giarrusso | |
| Copy change's variants in change_no_check, since supposedly they should all be supported. But they haven't been tested, and my example fails. | |||
| 2019-05-03 | Document _no_check tactics (#3225) | Paolo G. Giarrusso | |
| Triggered by trying to understand https://gitlab.mpi-sws.org/iris/iris/merge_requests/235. - Add a new section at the end - Document change_no_check, and convert_concl_no_check, address review comments | |||
| 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-05-01 | [comDefinition] Use prepare function from DeclareDef. | Emilio Jesus Gallego Arias | |
| We also update the plugin tutorial. This was already tried [in the same exact way] in #8811, however the bench time was not convincing then, but now things seem a bit better, likely due to the removal of some extra normalization somewhere. Some more changes from #8811 are still pending. | |||
| 2019-04-30 | Change entry from #9651. | Théo Zimmermann | |
| 2019-04-30 | Change entry for #10014. | Théo Zimmermann | |
| 2019-04-30 | Add number of commits, PRs and issues closed. | Théo Zimmermann | |
| 2019-04-30 | Advertize continuous deployment of documentation. | Théo Zimmermann | |
| 2019-04-30 | More review suggestions. | Théo Zimmermann | |
| 2019-04-30 | Remove remaining references to CHANGES.md from the Recent changes chapter. | Théo Zimmermann | |
| 2019-04-30 | Remove misplaced CHANGES entry and fix links formatting. | Théo Zimmermann | |
| PR #8187 misplaced its CHANGES entry. We remove it in this commit instead of moving it to the right place because it is reverted in #9987. | |||
| 2019-04-30 | Finish adding authors and links to PRs. | Théo Zimmermann | |
| 2019-04-30 | Change entry for #9906. | Théo Zimmermann | |
| 2019-04-30 | Split changes between main changes and other changes (no repetition). | Théo Zimmermann | |
| Add more links to PRs and credits of authors. | |||
| 2019-04-30 | Remove 8.10 entries from CHANGES file. | Théo Zimmermann | |
| 2019-04-30 | First fixing pass, and experiment with dune-style PR number and author listing. | Théo Zimmermann | |
| 2019-04-30 | Apply suggestions from code review | Théo Zimmermann | |
| Mainly markup fixes by Theo Co-Authored-By: mattam82 <matthieu.sozeau@inria.fr> | |||
| 2019-04-30 | Credits for 8.10 | Matthieu Sozeau | |
| 2019-04-30 | CoqIDE: updating documentation of the Preference windows. | Hugo Herbelin | |
| In particular, we explicitly mention the existence of an Emacs mode. | |||
| 2019-04-29 | Merge PR #9987: Fix #9180 by reverting #9249 and #8187 | Emilio Jesus Gallego Arias | |
| Reviewed-by: maximedenes | |||
| 2019-04-29 | Merge PR #9651: [ssr] Add tactics under and over | Cyril Cohen | |
| Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: erikmd Ack-by: gares Ack-by: jfehrle | |||
| 2019-04-29 | Merge PR #10011: [refman] Fix typo. | Vincent Laporte | |
| Reviewed-by: vbgl | |||
| 2019-04-29 | Merge PR #10018: Document unshelve (#3225) | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-04-29 | Revert #8187 | Vincent Laporte | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |