aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Collapse)Author
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
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
while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion).
2016-04-17Add changelog for 8.5pl1 after the fact.Maxime Dénès
Will be displayed on the website, but not part of the package.
2016-04-04Fix after merge, the revert of Bind Scope applies to trunk only.Matthieu Sozeau
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Matthieu Sozeau
into JasonGross-trunk-function_scope
2016-03-04All arguments defined through ARGUMENT EXTEND declare a tactic scope.Pierre-Marie Pédrot
Amongs other things, it kind of fixes bug #4492, even though you cannot really take advantage of the parsed data for now.
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these.
2016-01-21Fixing some problems with double induction.Hugo Herbelin
Basically, the hypotheses were treated in an incorrect order, with a hack for sometimes put them again in the right order, resulting in failures and redundant hypotheses. Status unclear, because this new version is incompatible except in simple cases like a double induction on two "nat". Fixing the bug incidentally simplify the code, relying on the deprecation since 8.4 to allow not to ensure a compatibility (beyond the simple situation of a double induction on simple datatypes). See file induct.v for effect of changes.
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Reporting about the new tactical unshelve.Hugo Herbelin
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
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
The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
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-11Merge branch 'v8.5'Pierre-Marie Pédrot
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
Marking it as experimental.
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal.
2015-12-05Fix CHANGES.Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-12Update CHANGESJason Gross
Mention compatibility file.
2015-11-11Fix bug #3735: interpretation of "->" in Program follows the standard one.Matthieu Sozeau
2015-11-10Listing separately changes from 8.5betas to final 8.5 and furtherHugo Herbelin
changes from final 8.5 to next version.
2015-11-10Activating bracketing of last or-and introduction pattern by defaultHugo Herbelin
for more regularity.
2015-11-05Update version numbers and magic numbers for 8.5beta3 release.Maxime Dénès
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
inconsistent).
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-21Mention bug 3199 fix as a source of incompatibilities.Matthieu Sozeau
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Documenting the option "Strict Universe Declaration" in CHANGES.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 08:08:22 +0000