aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2016-08-17Fixing CHANGES.Hugo Herbelin
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-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-20Update CHANGESMatthieu Sozeau
2016-07-08Add a few fixes in CHANGES that were forgotten.Maxime Dénès
2016-07-05congruence fix: test-suite code and update CHANGESMatthieu Sozeau
2016-07-04Mention more fixes in CHANGES before we release pl2.Maxime Dénès
2016-06-27Univs/CHANGES: #4097 and annotations on notationsMatthieu Sozeau
2016-06-09Reporting about a few bug fixes (to be continued).Hugo Herbelin
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
2016-04-22Mention problems with fix of #4582 in CHANGES.Maxime Dénès
2016-04-22Mention #4548 (fixed) in CHANGES.Maxime Dénès
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-04-17Add changelog for 8.5pl1 after the fact.Maxime Dénès
2016-01-12Reporting about the new tactical unshelve.Hugo Herbelin
2015-12-16Update version numbers and magic numbers for 8.5rc1 release.Maxime Dénès
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-14Updating CHANGES with an incompatibility.Hugo Herbelin
2015-12-14Flag -compat 8.4 now loads Coq.Compat.Coq84.Maxime Dénès
2015-12-11Document removal of Set Virtual Machine and -vm in CHANGES.Maxime Dénès
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-05Fix CHANGES.Hugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-12Update CHANGESJason Gross
2015-11-11Fix bug #3735: interpretation of "->" in Program follows the standard one.Matthieu Sozeau
2015-11-05Update version numbers and magic numbers for 8.5beta3 release.Maxime Dénès
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-21Mention bug 3199 fix as a source of incompatibilities.Matthieu Sozeau
2015-10-19Documenting the option "Strict Universe Declaration" in CHANGES.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
2015-09-16Explain new flags for native_compute in CHANGES.Maxime Dénès
2015-09-08New option "Unset Bracketing Last Introduction Pattern" for preservingHugo Herbelin
2015-08-02Granting Jason's request for an ad hoc compatibility option onHugo Herbelin
2015-08-02Documenting change of behavior of apply when the lemma is a tuple andHugo Herbelin
2015-07-10Rewording about how to upgrade on failing calls to constructor.Hugo Herbelin
2015-07-10CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla.Maxime Dénès
2015-07-05More precise rewording about asymmetric patterns.Hugo Herbelin
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-18Fixed CHANGES to reflect -color option.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 12:52:36 +0000