Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | 2017-05-17 |
|\ | |||
* | | Aligning on standard layout of CHANGES. | Hugo Herbelin | 2017-05-13 |
| | | |||
| * | Documenting Printing Compact Contexts + CHANGES | Pierre Courtieu | 2017-05-11 |
| | | |||
* | | Tentative note in CHANGES about now applying βι while typing "match" branches. | Hugo Herbelin | 2017-04-27 |
|/ | | | | | | | In practice, this is almost invisible except when using "refine". So, in some sense, it is aligning the behavior of pretyping on the one of logic.ml's "refine" so that the more natural behavior of 8.4's refine on this issue is restored. | ||
* | CHANGES entry for #545. | Maxime Dénès | 2017-04-19 |
| | |||
* | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | 2017-04-11 |
|\ | |||
| * | Documenting the changes introduced by the EConstr branch. | Pierre-Marie Pédrot | 2017-04-10 |
| | | |||
* | | [camlpX] Enrico's changes to camlp4 removal. | Emilio Jesus Gallego Arias | 2017-04-07 |
|/ | | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change. | ||
* | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 |
|\ | |||
* | | Document the changes to IZR. | Guillaume Melquiond | 2017-03-22 |
| | | |||
| * | Farewell decl_mode | Enrico Tassi | 2017-03-07 |
| | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | ||
* | | CHANGES: choice over setoids and prop. ext. | Hugo Herbelin | 2017-03-03 |
|/ | |||
* | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-01-19 |
|\ | |||
| * | A few words in CHANGES. | Maxime Dénès | 2016-12-07 |
| | | |||
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-30 |
|\| | |||
| * | Fix some documentation typos. | Guillaume Melquiond | 2016-11-24 |
| | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | ||
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 |
|\| | |||
| * | [doc] Mention XML protocol on changes. | Emilio Jesus Gallego Arias | 2016-11-16 |
| | | | | | | | | It may be worth it, also added a note about file reorganization. | ||
| * | Remove the list of bug fixes from CHANGES. | Maxime Dénès | 2016-11-14 |
| | | | | | | | | | | We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear. | ||
| * | Update CHANGES and credits for 8.6beta1. | Maxime Dénès | 2016-11-10 |
| | | |||
| * | Mention notypeclasses refine in CHANGES | Matthieu Sozeau | 2016-11-07 |
| | | |||
| * | CHANGES for this branch. | Matthieu Sozeau | 2016-11-07 |
| | | |||
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-29 |
|\| | |||
| * | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-26 |
| |\ | |||
| | * | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | 2016-10-25 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses. | ||
| | * | Update CHANGES. | Maxime Dénès | 2016-10-25 |
| | | | |||
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-12 |
|\| | | |||
* | | | Allocating a section in CHANGES for changes specific to 8.7. | Hugo Herbelin | 2016-10-12 |
| | | | |||
| * | | Tentatively preparing to add changes specific to v8.7 (see PR #275). | Hugo Herbelin | 2016-10-12 |
|/ / | |||
* | | Report about changes of semantics of auto as an ltac argument (see #4966). | Hugo Herbelin | 2016-10-08 |
| | | |||
* | | Remove the Set Verbose Compat option and turn the warning on by default. | Maxime Dénès | 2016-10-06 |
| | | | | | | | | | | These warnings can now be configured like any other, so we don't need a specific option anymore. | ||
* | | Document change related to Keep Proof Equalities in CHANGES. | Maxime Dénès | 2016-10-03 |
| | | |||
* | | Being more informative about the change of behavior of "subst". | Hugo Herbelin | 2016-09-29 |
| | | |||
* | | Fix description of change in intro semantics. | Maxime Dénès | 2016-09-21 |
| | | |||
* | | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵ | Hugo Herbelin | 2016-09-15 |
| | | | | | | | | | | | | | | | | | | | | ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5. | ||
* | | Refolding: disable in 8.4 compat file, document | Matthieu Sozeau | 2016-09-12 |
| | | |||
* | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-08-21 |
|\| | |||
| * | Fixing CHANGES. | Hugo Herbelin | 2016-08-17 |
| | | | | | | | | | | Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section. | ||
* | | Documenting fix of #3070 (subst and chain of dependencies). | Hugo Herbelin | 2016-08-17 |
| | | |||
* | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-08-16 |
|\| | |||
| * | Fix #5000: Document the native compiler soundness bug due to Unicode mangling. | Pierre-Marie Pédrot | 2016-08-07 |
| | | |||
| * | Fix bug #4673: regression in setoid_rewrite. | Matthieu Sozeau | 2016-07-29 |
| | | | | | | | | Modulo delta for types should be fully transparent. | ||
* | | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | 2016-07-29 |
|\| | |||
| * | Update CHANGES about #3886 bugfix | Matthieu Sozeau | 2016-07-29 |
| | | |||
| * | Fix #4769, univ poly and elim schemes in sections | Matthieu Sozeau | 2016-07-29 |
| | | |||
| * | Update CHANGES about critical bugfix and others | Matthieu Sozeau | 2016-07-26 |
| | | |||
* | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-07-20 |
|\| | |||
| * | Update CHANGES | Matthieu Sozeau | 2016-07-20 |
| | | |||
* | | Update CHANGES | Matthieu Sozeau | 2016-07-20 |
| | | |||
* | | A new step on using alpha-conversion in printing notations. | Hugo Herbelin | 2016-07-18 |
| | | | | | | | | | | | | | | A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns). |