aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Update CHANGES about #3886 bugfixMatthieu Sozeau
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-26Update CHANGES about critical bugfix and othersMatthieu Sozeau
2016-07-20Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-20Update CHANGESMatthieu Sozeau
2016-07-20Update CHANGESMatthieu Sozeau
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-08Add a few fixes in CHANGES that were forgotten.Maxime Dénès
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-05congruence fix: test-suite code and update CHANGESMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 10:18:21 +0000