aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Collapse)Author
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
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-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Allocating a section in CHANGES for changes specific to 8.7.Hugo Herbelin
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
2016-06-16Document new Hint Mode option.Matthieu Sozeau
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
As noticed by C. Cohen it was confusingly different from standard notation.
2016-06-16Not taking arguments given by name or position into account whenHugo Herbelin
computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available. For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _", the same way as if we had said: Arguments eq_refl {A} {x}.
2016-06-16Merge PR #195: Complete is_* family of term-examining tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:06:05 +0000