aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\
* | Update CHANGES, the bugfixes for 4527 and 4726 areGravatar Matthieu Sozeau2016-07-04
| * Mention more fixes in CHANGES before we release pl2.Gravatar Maxime Dénès2016-07-04
* | Updated CHANGES about subst. More on recursive equations in reference manual.Gravatar Hugo Herbelin2016-06-29
* | CHANGES: document fix for #4726 too.Gravatar Matthieu Sozeau2016-06-29
* | CHANGES: document fix for 4527 and compatibility.Gravatar Matthieu Sozeau2016-06-29
* | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \
| | * Univs/CHANGES: #4097 and annotations on notationsGravatar Matthieu Sozeau2016-06-27
* | | Update CHANGES and COMPATIBILITYGravatar Matthieu Sozeau2016-06-27
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * | Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
|/ /
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* | Mentioning goal selectors in CHANGESGravatar Enrico Tassi2016-06-17
* | Fix wrong tabulation in CHANGESGravatar Matthieu Sozeau2016-06-16
* | Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
* | Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-06-16
* | Merge PR #195: Complete is_* family of term-examining tactics.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
* | | --print-version produces machine readable version infoGravatar Enrico Tassi2016-06-16
| * | Update CHANGESGravatar Jason Gross2016-06-16
* | | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\ \ \ \ | |_|/ / |/| | / | | |/ | |/|
| * | Reporting about a few bug fixes (to be continued).Gravatar Hugo Herbelin2016-06-09
* | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| |/ |/|
* | 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
* | 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
| * Add changelog for 8.5pl1 after the fact.Gravatar Maxime Dénès2016-04-17
* | 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 into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* | | All arguments defined through ARGUMENT EXTEND declare a tactic scope.Gravatar Pierre-Marie Pédrot2016-03-04
* | | 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
* | | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
* | | 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
* | | 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
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 10:20:57 +0000