| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2019-02-01 | Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zify | Vincent 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-24 | Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, ↵ | Jason Gross | |
| Z.to_euclidean_division_equations | |||
| 2019-01-24 | Revert "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-24 | Add subst to the end of nia in the test-suite | Jason 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-24 | Don't bundle Z.div_mod_quot_rem into zify | Jason 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`. | |||
| 2019-01-24 | Add Z.div_mod_to_quot_rem tactic, put it in zify | Jason Gross | |
| The various (micr)omega tactics now support `Z.div` and `Z.modulo`. I briefly looked into supporting `Nat.div` and `Nat.modulo`, but the conversions between `Z.div` and `Nat.div` are defined in `ZArith.Zdiv`, which depends on `Omega`, which depends on `PreOmega`, which is where `zify` is defined. | |||
| 2019-01-22 | Remove unneeded | in productionlists | Jim Fehrle | |
| 2018-12-04 | Add undocumented options from mattam82 | Jim Fehrle | |
| 2018-12-04 | Document undocumented flags and options | Jim Fehrle | |
| Also remove a few undocumented settings | |||
| 2018-12-03 | A few fixes of unexisting tokens. | Théo Zimmermann | |
| 2018-12-03 | Closes #9118: single backticks are made equivalent to double backticks; try ↵ | Théo Zimmermann | |
| to fix all misuses. | |||
| 2018-11-30 | Add indexes for coercion / substructure symbol :>. | Théo Zimmermann | |
| And a few more Sphinx fixes in passing. | |||
| 2018-11-28 | Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a class | Matthieu Sozeau | |
| 2018-11-27 | Merge PR #8850: Private universes for opaque polymorphic constants. | Matthieu Sozeau | |
| 2018-11-27 | [Typeclasses] Warn when RHS of `:>` is not a class | Vincent Laporte | |
| This introduces the warning “not-a-class” in the “typeclasses” category. | |||
| 2018-11-25 | Merge PR #9036: Add bodies to sphinx objects. | Clément Pit-Claudel | |
| 2018-11-23 | Doc for Private Polymorphic Universes. | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |