aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * Mention problems with fix of #4582 in CHANGES.Gravatar Maxime Dénès2016-04-22
| |
| * Mention #4548 (fixed) in CHANGES.Gravatar Maxime Dénès2016-04-22
| |
| * Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
| | | | | | | | | | while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion).
| * Add changelog for 8.5pl1 after the fact.Gravatar Maxime Dénès2016-04-17
| | | | | | | | Will be displayed on the website, but not part of the package.
* | Fix after merge, the revert of Bind Scope applies to trunk only.Gravatar Matthieu Sozeau2016-04-04
| |
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ | | | | | | | | | into JasonGross-trunk-function_scope
* | | All arguments defined through ARGUMENT EXTEND declare a tactic scope.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | | | | | | | | | | Amongs other things, it kind of fixes bug #4492, even though you cannot really take advantage of the parsed data for now.
* | | Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
| | |
* | | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\ \ \ | | |/ | |/|
| * | Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\| |
| * | Update version numbers and magic numbers for 8.5rc1 release.Gravatar Maxime Dénès2015-12-16
| | |
| * | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
| | |
| * | Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
| | | | | | | | | | | | | | | | | | 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.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\| |
| * | Updating CHANGES with an incompatibility.Gravatar Hugo Herbelin2015-12-14
| | |
| * | Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\| |
| * | Document removal of Set Virtual Machine and -vm in CHANGES.Gravatar Maxime Dénès2015-12-11
| | |
| * | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
| | | | | | | | | | | | Marking it as experimental.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\| |
| * | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Fix CHANGES.Gravatar Hugo Herbelin2015-12-05
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\| |
| * | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\| |
| * | Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
| | | | | | | | | | | | | | | constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-15
|\| |
| * | Update CHANGESGravatar Jason Gross2015-11-12
| | | | | | | | | | | | Mention compatibility file.
| * | Fix bug #3735: interpretation of "->" in Program follows the standard one.Gravatar Matthieu Sozeau2015-11-11
| | |
* | | Listing separately changes from 8.5betas to final 8.5 and furtherGravatar Hugo Herbelin2015-11-10
| | | | | | | | | | | | changes from final 8.5 to next version.
* | | Activating bracketing of last or-and introduction pattern by defaultGravatar Hugo Herbelin2015-11-10
| | | | | | | | | | | | for more regularity.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\| |
| * | Update version numbers and magic numbers for 8.5beta3 release.Gravatar Maxime Dénès2015-11-05
| | |
| * | Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
| | | | | | | | | | | | inconsistent).
| * | Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-26
|\| |
| * | Mention bug 3199 fix as a source of incompatibilities.Gravatar Matthieu Sozeau2015-10-21
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\| |
| * | Documenting the option "Strict Universe Declaration" in CHANGES.Gravatar Pierre-Marie Pédrot2015-10-19
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\| |
| * | Fix some typos.Gravatar Guillaume Melquiond2015-10-13
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\| |
| * | Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 04:56:03 +0000