aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2016-12-07A few words in CHANGES.Maxime Dénès
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-16[doc] Mention XML protocol on changes.Emilio Jesus Gallego Arias
2016-11-14Remove the list of bug fixes from CHANGES.Maxime Dénès
2016-11-10Update CHANGES and credits for 8.6beta1.Maxime Dénès
2016-11-07Mention notypeclasses refine in CHANGESMatthieu Sozeau
2016-11-07CHANGES for this branch.Matthieu Sozeau
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-25Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Maxime Dénès
2016-10-25Update CHANGES.Maxime Dénès
2016-10-12Tentatively preparing to add changes specific to v8.7 (see PR #275).Hugo Herbelin
2016-10-08Report about changes of semantics of auto as an ltac argument (see #4966).Hugo Herbelin
2016-10-06Remove the Set Verbose Compat option and turn the warning on by default.Maxime Dénès
2016-10-03Document change related to Keep Proof Equalities in CHANGES.Maxime Dénès
2016-09-29Being more informative about the change of behavior of "subst".Hugo Herbelin
2016-09-21Fix description of change in intro semantics.Maxime Dénès
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-09-12Refolding: disable in 8.4 compat file, documentMatthieu Sozeau
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-17Fixing CHANGES.Hugo Herbelin
2016-08-17Documenting fix of #3070 (subst and chain of dependencies).Hugo Herbelin
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-07Fix #5000: Document the native compiler soundness bug due to Unicode mangling.Pierre-Marie Pédrot
2016-07-29Fix bug #4673: regression in setoid_rewrite.Matthieu Sozeau
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Update CHANGES about #3886 bugfixMatthieu Sozeau
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-26Update CHANGES about critical bugfix and othersMatthieu Sozeau
2016-07-20Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-20Update CHANGESMatthieu Sozeau
2016-07-20Update CHANGESMatthieu Sozeau
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-08Add a few fixes in CHANGES that were forgotten.Maxime Dénès
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-05congruence fix: test-suite code and update CHANGESMatthieu Sozeau
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-04Update CHANGES, the bugfixes for 4527 and 4726 areMatthieu Sozeau
2016-07-04Mention more fixes in CHANGES before we release pl2.Maxime Dénès
2016-06-29Updated CHANGES about subst. More on recursive equations in reference manual.Hugo Herbelin
2016-06-29CHANGES: document fix for #4726 too.Matthieu Sozeau
2016-06-29CHANGES: document fix for 4527 and compatibility.Matthieu Sozeau
2016-06-28Merge remote-tracking branch 'github/pr/207' into trunkMaxime Dénès
2016-06-27Univs/CHANGES: #4097 and annotations on notationsMatthieu Sozeau
2016-06-27Update CHANGES and COMPATIBILITYMatthieu Sozeau
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-19Add [Unset Printing Dependent Evars Line]Jason Gross
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-17Mentioning goal selectors in CHANGESEnrico Tassi
2016-06-16Fix wrong tabulation in CHANGESMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 22:55:07 +0000