Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Documenting the changes introduced by the EConstr branch. | 2017-04-10 | ||
| | | ||||
* | | [camlpX] Enrico's changes to camlp4 removal. | 2017-04-07 | ||
|/ | | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change. | |||
* | Merge PR#455: Farewell decl_mode | 2017-04-06 | ||
|\ | ||||
* | | Document the changes to IZR. | 2017-03-22 | ||
| | | ||||
| * | Farewell decl_mode | 2017-03-07 | ||
| | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | |||
* | | CHANGES: choice over setoids and prop. ext. | 2017-03-03 | ||
|/ | ||||
* | Merge branch 'v8.6' | 2017-01-19 | ||
|\ | ||||
| * | A few words in CHANGES. | 2016-12-07 | ||
| | | ||||
* | | Merge branch 'v8.6' | 2016-11-30 | ||
|\| | ||||
| * | Fix some documentation typos. | 2016-11-24 | ||
| | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | |||
* | | Merge branch 'v8.6' | 2016-11-18 | ||
|\| | ||||
| * | [doc] Mention XML protocol on changes. | 2016-11-16 | ||
| | | | | | | | | It may be worth it, also added a note about file reorganization. | |||
| * | Remove the list of bug fixes from CHANGES. | 2016-11-14 | ||
| | | | | | | | | | | We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear. | |||
| * | Update CHANGES and credits for 8.6beta1. | 2016-11-10 | ||
| | | ||||
| * | Mention notypeclasses refine in CHANGES | 2016-11-07 | ||
| | | ||||
| * | CHANGES for this branch. | 2016-11-07 | ||
| | | ||||
* | | Merge branch 'v8.6' | 2016-10-29 | ||
|\| | ||||
| * | Merge branch 'v8.5' into v8.6 | 2016-10-26 | ||
| |\ | ||||
| | * | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | 2016-10-25 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | |||
| | * | Update CHANGES. | 2016-10-25 | ||
| | | | ||||
* | | | Merge branch 'v8.6' | 2016-10-12 | ||
|\| | | ||||
* | | | Allocating a section in CHANGES for changes specific to 8.7. | 2016-10-12 | ||
| | | | ||||
| * | | Tentatively preparing to add changes specific to v8.7 (see PR #275). | 2016-10-12 | ||
|/ / | ||||
* | | Report about changes of semantics of auto as an ltac argument (see #4966). | 2016-10-08 | ||
| | | ||||
* | | Remove the Set Verbose Compat option and turn the warning on by default. | 2016-10-06 | ||
| | | | | | | | | | | These warnings can now be configured like any other, so we don't need a specific option anymore. | |||
* | | Document change related to Keep Proof Equalities in CHANGES. | 2016-10-03 | ||
| | | ||||
* | | Being more informative about the change of behavior of "subst". | 2016-09-29 | ||
| | | ||||
* | | Fix description of change in intro semantics. | 2016-09-21 | ||
| | | ||||
* | | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵ | 2016-09-15 | ||
| | | | | | | | | | | | | | | | | | | | | ~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. | |||
* | | Refolding: disable in 8.4 compat file, document | 2016-09-12 | ||
| | | ||||
* | | Merge branch 'v8.5' into v8.6 | 2016-08-21 | ||
|\| | ||||
| * | Fixing CHANGES. | 2016-08-17 | ||
| | | | | | | | | | | Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section. | |||
* | | Documenting fix of #3070 (subst and chain of dependencies). | 2016-08-17 | ||
| | | ||||
* | | Merge branch 'v8.5' into v8.6 | 2016-08-16 | ||
|\| | ||||
| * | Fix #5000: Document the native compiler soundness bug due to Unicode mangling. | 2016-08-07 | ||
| | | ||||
| * | Fix bug #4673: regression in setoid_rewrite. | 2016-07-29 | ||
| | | | | | | | | Modulo delta for types should be fully transparent. | |||
* | | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | 2016-07-29 | ||
|\| | ||||
| * | Update CHANGES about #3886 bugfix | 2016-07-29 | ||
| | | ||||
| * | Fix #4769, univ poly and elim schemes in sections | 2016-07-29 | ||
| | | ||||
| * | Update CHANGES about critical bugfix and others | 2016-07-26 | ||
| | | ||||
* | | Merge branch 'v8.5' into v8.6 | 2016-07-20 | ||
|\| | ||||
| * | Update CHANGES | 2016-07-20 | ||
| | | ||||
* | | Update CHANGES | 2016-07-20 | ||
| | | ||||
* | | A new step on using alpha-conversion in printing notations. | 2016-07-18 | ||
| | | | | | | | | | | | | | | 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). | |||
* | | Merge branch 'v8.5' into v8.6 | 2016-07-13 | ||
|\| | ||||
| * | Add a few fixes in CHANGES that were forgotten. | 2016-07-08 | ||
| | | | | | | | | We should really automate the generation of the log of fixes for CHANGES. | |||
* | | Merge branch 'v8.5' into v8.6 | 2016-07-07 | ||
|\| | ||||
| * | congruence fix: test-suite code and update CHANGES | 2016-07-05 | ||
| | | | | | | | | This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718. | |||
* | | Merge branch 'v8.5' into trunk | 2016-07-04 | ||
|\| | ||||
* | | Update CHANGES, the bugfixes for 4527 and 4726 are | 2016-07-04 | ||
| | | | | | | | | not in pl2. |