aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Collapse)Author
2016-12-07A few words in CHANGES.Maxime Dénès
2016-11-24Fix some documentation typos.Guillaume Melquiond
Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
2016-11-16[doc] Mention XML protocol on changes.Emilio Jesus Gallego Arias
It may be worth it, also added a note about file reorganization.
2016-11-14Remove the list of bug fixes from CHANGES.Maxime Dénès
We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear.
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
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.
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
These warnings can now be configured like any other, so we don't need a specific option anymore.
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
~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.
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
Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section.
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
Modulo delta for types should be fully transparent.
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
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).
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
We should really automate the generation of the log of fixes for CHANGES.
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-05congruence fix: test-suite code and update CHANGESMatthieu Sozeau
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-04Update CHANGES, the bugfixes for 4527 and 4726 areMatthieu Sozeau
not in pl2.
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
Was PR#207: Add -no-print-dependent-evars
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
Cf CHANGES for details.
2016-06-19Add [Unset Printing Dependent Evars Line]Jason Gross
This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
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-06-12 16:55:37 +0000