aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-04Update CHANGES, the bugfixes for 4527 and 4726 areMatthieu Sozeau
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
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
2016-06-19Add [Unset Printing Dependent Evars Line]Jason Gross
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
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
2016-06-16Not taking arguments given by name or position into account whenHugo Herbelin
2016-06-16Merge PR #195: Complete is_* family of term-examining tactics.Pierre-Marie Pédrot
2016-06-16--print-version produces machine readable version infoEnrico Tassi
2016-06-16Update CHANGESJason Gross
2016-06-14Merge remote-tracking branch 'origin/pr/166' into trunkEnrico Tassi
2016-06-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-09Reporting about a few bug fixes (to be continued).Hugo Herbelin
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
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
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
2016-04-17Add changelog for 8.5pl1 after the fact.Maxime Dénès
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 into...Matthieu Sozeau
2016-03-04All arguments defined through ARGUMENT EXTEND declare a tactic scope.Pierre-Marie Pédrot
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
2016-01-21Fixing some problems with double induction.Hugo Herbelin
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
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
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:41:49 +0000