| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle | |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-11-24 | Convert auto chapter to prodn | Jim Fehrle | |
| 2020-11-20 | Use nat_or_var where negative values don't make sense | Jim Fehrle | |
| 2020-11-18 | [attributes] Deprecate `attr(true)` syntax in favor of booelan attributes. | Emilio Jesus Gallego Arias | |
| We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog. | |||
| 2020-11-16 | Merge PR #13188: Default disable automatic generalization of Instance type | Pierre-Marie Pédrot | |
| Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot | |||
| 2020-11-15 | Doc and changelog for Instance Generalized Output | Gaëtan Gilbert | |
| 2020-11-14 | Distinguish one_pattern and one_term nonterminals | Jim Fehrle | |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann | |
| The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version. | |||
| 2020-10-24 | Convert misc chapters to prodn | Jim Fehrle | |
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann | |
| 2020-09-27 | Reduce nitpick_ignore list a little. | Théo Zimmermann | |
| 2020-09-11 | [refman] Rename num to natural | Pierre Roux | |
| 2020-04-26 | Convert syntax extensions chapter to prodn | Jim Fehrle | |
| 2020-03-19 | Document all the existing attributes. | Théo Zimmermann | |
| And fix documentation following the removal of the Template Check flag in #11546. | |||
| 2020-03-13 | Implementing postponed constraints in TC resolution | Matthieu Sozeau | |
| A constraint can be stuck if it does not match any of the declared modes for its head (if there are any). In that case, the subgoal is postponed and the next ones are tried. We do a fixed point computation until there are no stuck subgoals or the set does not change (it is impossible to make it grow, as asserted in the code, because it is always a subset of the initial goals) This allows constraints on classes with modes to be treated as if they were in any order (yay for stability of solutions!). Also, ultimately it should free us to launch resolutions more agressively (avoiding issues like the ones seen in PR #10762). Add more examples of the semantics of TC resolution with apply in test-suite Properly catch ModeMatchFailure on calls to map_e* Add fixed bug 9058 to the test-suite Close #9058 Add documentation Fixes after Gaëtan's review. Main change is to not use exceptions for control-flow Update tactics/class_tactics.ml Clearer and more efficient mode mismatch dispatch Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> Remove exninfo argument | |||
| 2020-02-28 | Convert Gallina Vernac to use prodn | Jim Fehrle | |
| 2019-11-29 | Remove deprecated Typeclasses Axioms Are Instances. | Théo Zimmermann | |
| 2019-11-20 | Merge PR #11119: 8.10-backportable part of #10575 | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel | |||
| 2019-11-14 | Restore documentation of `Typeclasses Axioms Are Instances` | Maxime Dénès | |
| This documentation seems to have been lost after it was introduced by 0ad26633a4589d77de1f864733d1d953dab9ea91 We also document that this flag is deprecated. | |||
| 2019-11-13 | Return of Refine Instance as an attribute. | Gaëtan Gilbert | |
| We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm. | |||
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle | |
| 2019-07-05 | Correct doc about default value for Typeclasses Dependency Order | Gaëtan Gilbert | |
| 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-16 | [refman] Introduce syntax for alternatives in notations | Clément Pit-Claudel | |
| Closes GH-8482. | |||
| 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-27 | Minor doc improvement. | Théo Zimmermann | |
| 2019-04-27 | [refman] Fix typo. | Théo Zimmermann | |
| Noticed by Maxime Dénès. | |||
| 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-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-02-18 | Fix doc for Refine Instance Mode | Gaëtan Gilbert | |
| 2019-02-18 | Fix failing coqtops in type-classes.rst | Gaëtan Gilbert | |
| 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-11-30 | Add indexes for coercion / substructure symbol :>. | Théo Zimmermann | |
| And a few more Sphinx fixes in passing. | |||
| 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-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 2018-09-20 | Rewrite "Flags, Options and Tables" section. | Jim Fehrle | |
| Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag: | |||
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-08-31 | Fixed the seealso directive in a few places. | Zeimer | |
| 2018-08-31 | Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵ | Zeimer | |
| directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues. | |||
| 2018-08-01 | Improved grammar and spelling in chapters 'Type Classes', 'Omega' and ↵ | Zeimer | |
| 'Micromega' of the Reference Manual. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |