| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | 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-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 | |
| 2019-04-29 | Document unshelve (#3225) | Paolo G. Giarrusso | |
| I believe this is the appropriate place for users to read about this, even tho `unshelve` is technically a tactical. This example was explicitly requested in #3225 and is commonly used in both Iris (and was documented in the changelog at the time). | |||
| 2019-04-28 | Merge PR #9605: [coq_makefile] Enforce warn_error for plugins. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares | |||
| 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-24 | Merge PR #9988: [refman] Properly define token regexp. | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel | |||
| 2019-04-24 | [refman] Fix a quoting problem. | Théo Zimmermann | |
| 2019-04-24 | [refman] Properly define token regexp. | Théo Zimmermann | |
| 2019-04-24 | [coq_makefile] Enforce warn_error for plugins. | Emilio Jesus Gallego Arias | |
| The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974 | |||
| 2019-04-23 | [ssr] under: optimization of the tactic for (under eq_bigl => *) | Erik Martin-Dorel | |
| so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|]. Also: replace "by over." in the doc example with "over." | |||
| 2019-04-23 | [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations | Erik Martin-Dorel | |
| as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation. | |||
| 2019-04-23 | [doc] ssr_under: a few improvements | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |