| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-26 | Move Classes.tex to type-classes.rst | Matthieu Sozeau | |
| 2018-03-22 | Merge branch 'master' into sphinx-doc-chapter-22 | Guillaume Melquiond | |
| 2018-03-22 | Merge branch 'master' into sphinx-doc-chapter-21 | Guillaume Melquiond | |
| 2018-03-22 | Merge branch 'master' into sphinx-doc-chapter-19 | Guillaume Melquiond | |
| 2018-03-22 | [Sphinx] Move chapter 22 to new infrastructure | Maxime Dénès | |
| 2018-03-22 | [Sphinx] Move chapter 21 to new infrastructure | Maxime Dénès | |
| 2018-03-22 | [Sphinx] Move chapter 19 to new infrastructure | Maxime Dénès | |
| 2018-03-22 | [Sphinx] Move chapter 17 to new infrastructure | Maxime Dénès | |
| 2018-03-16 | [Sphinx] Add chapter 11 | Maxime Dénès | |
| Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 3 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 16 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 14 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 13 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 12 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 10 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 8 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 5 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 4 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 2 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move credits to new infrastructure | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Move introduction to new infrastructure | Maxime Dénès | |
| 2018-03-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 2018-03-09 | Documentation for Cumulativity Weak Constraints. | Gaëtan Gilbert | |
| 2018-03-09 | Merge PR #6480: Allow Prop as source for coercions | Maxime Dénès | |
| 2018-03-09 | Merge PR #6895: [compat] Remove "Refolding Reduction" option. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | |
| 2018-03-09 | doc and changes for coercion from prop/type | charguer | |
| 2018-03-08 | [compat] Remove "Refolding Reduction" option. | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895. | |||
| 2018-03-08 | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès | |
| 2018-03-08 | Merge PR #6582: Mangle auto-generated names | Maxime Dénès | |
| 2018-03-06 | [compat] Remove "Shrink Abstract" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we the option "Shrink Abstract". | |||
| 2018-03-06 | Merge PR #6896: [compat] Remove NOOP deprecated options. | Maxime Dénès | |
| 2018-03-06 | Merge PR #6824: Remove deprecated options related to typeclasses. | Maxime Dénès | |
| 2018-03-06 | Merge PR #6898: [compat] Remove "Intuition Iff Unfolding" | Maxime Dénès | |
| 2018-03-05 | Deprecate Focus and Unfocus. | Théo Zimmermann | |
| 2018-03-04 | [compat] Remove NOOP and alias deprecated options. | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP. | |||
| 2018-03-04 | Remove deprecated options related to typeclasses. | Théo Zimmermann | |
| 2018-03-04 | Merge PR #915: Fix rewrite in * side conditions | Maxime Dénès | |
| 2018-03-04 | Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵ | Maxime Dénès | |
| supported scenarios. | |||
| 2018-03-04 | Fix typos. | Théo Zimmermann | |
| 2018-03-03 | [compat] Remove "Intuition Iff Unfolding" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove the option "Intuition Iff Unfolding" | |||
| 2018-03-01 | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | Hugo Herbelin | |
| Noticed by Sigurd Schneider. | |||
| 2018-02-28 | Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). | Hugo Herbelin | |
| 2018-02-28 | [toplevel] [vernac] Remove Load hack and check supported scenarios. | Emilio Jesus Gallego Arias | |
| Parsing in `VernacLoad` was broken for a while, but the situation has improved by miscellaneous refactoring. However, we still cannot support `Load` properly when proofs are crossing file boundaries. So in this patch we do two things: - We check for supported scenarios [no proofs open at `Load` entry/exit] - Remove the hack in `toplevel` so the behavior of `Load` is consistent between `coqide`/`coqc`. We close #5053 as its main bug was fixed by the main toplevel refactoring and the remaining cases are documented now. | |||
| 2018-02-27 | Typo in the documentation of the `pattern` tactic | Joachim Breitner | |
| 2018-02-22 | Document Arguments extra scopes flag | Jasper Hugunin | |
| 2018-02-20 | Documenting use of primitive entry names for restricting syntax in notations. | Hugo Herbelin | |
| 2018-02-20 | Extended documentation for notations referring to binders. | Hugo Herbelin | |
| Talking about the difference between ident and pattern. Giving examples. | |||
| 2018-02-20 | A first step at refreshing and documenting the new feature. | Hugo Herbelin | |
| 2018-02-17 | Implement name mangling option | Jasper Hugunin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |