aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* CHANGES: choice over setoids and prop. ext.Gravatar Hugo Herbelin2017-03-03
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\
| * A few words in CHANGES.Gravatar Maxime Dénès2016-12-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * [doc] Mention XML protocol on changes.Gravatar Emilio Jesus Gallego Arias2016-11-16
| * Remove the list of bug fixes from CHANGES.Gravatar Maxime Dénès2016-11-14
| * Update CHANGES and credits for 8.6beta1.Gravatar Maxime Dénès2016-11-10
| * Mention notypeclasses refine in CHANGESGravatar Matthieu Sozeau2016-11-07
| * CHANGES for this branch.Gravatar Matthieu Sozeau2016-11-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\
| | * Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Gravatar Maxime Dénès2016-10-25
| | * Update CHANGES.Gravatar Maxime Dénès2016-10-25
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
* | | Allocating a section in CHANGES for changes specific to 8.7.Gravatar Hugo Herbelin2016-10-12
| * | Tentatively preparing to add changes specific to v8.7 (see PR #275).Gravatar Hugo Herbelin2016-10-12
|/ /
* | Report about changes of semantics of auto as an ltac argument (see #4966).Gravatar Hugo Herbelin2016-10-08
* | Remove the Set Verbose Compat option and turn the warning on by default.Gravatar Maxime Dénès2016-10-06
* | Document change related to Keep Proof Equalities in CHANGES.Gravatar Maxime Dénès2016-10-03
* | Being more informative about the change of behavior of "subst".Gravatar Hugo Herbelin2016-09-29
* | Fix description of change in intro semantics.Gravatar Maxime Dénès2016-09-21
* | Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\|
| * Fixing CHANGES.Gravatar Hugo Herbelin2016-08-17
* | Documenting fix of #3070 (subst and chain of dependencies).Gravatar Hugo Herbelin2016-08-17
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\|
| * Fix #5000: Document the native compiler soundness bug due to Unicode mangling.Gravatar Pierre-Marie Pédrot2016-08-07
| * Fix bug #4673: regression in setoid_rewrite.Gravatar Matthieu Sozeau2016-07-29
* | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\|
| * Update CHANGES about #3886 bugfixGravatar Matthieu Sozeau2016-07-29
| * Fix #4769, univ poly and elim schemes in sectionsGravatar Matthieu Sozeau2016-07-29
| * Update CHANGES about critical bugfix and othersGravatar Matthieu Sozeau2016-07-26
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-20
|\|
| * Update CHANGESGravatar Matthieu Sozeau2016-07-20
* | Update CHANGESGravatar Matthieu Sozeau2016-07-20
* | A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-13
|\|
| * Add a few fixes in CHANGES that were forgotten.Gravatar Maxime Dénès2016-07-08
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\|
| * congruence fix: test-suite code and update CHANGESGravatar Matthieu Sozeau2016-07-05
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\|
* | Update CHANGES, the bugfixes for 4527 and 4726 areGravatar Matthieu Sozeau2016-07-04
| * Mention more fixes in CHANGES before we release pl2.Gravatar Maxime Dénès2016-07-04
* | Updated CHANGES about subst. More on recursive equations in reference manual.Gravatar Hugo Herbelin2016-06-29
* | CHANGES: document fix for #4726 too.Gravatar Matthieu Sozeau2016-06-29
* | CHANGES: document fix for 4527 and compatibility.Gravatar Matthieu Sozeau2016-06-29
* | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \