aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
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
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
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
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-12Update CHANGESJason Gross
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
2015-11-10Activating bracketing of last or-and introduction pattern by defaultHugo Herbelin
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
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
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-16Explain new flags for native_compute in CHANGES.Maxime Dénès
2015-09-09Merge remote-tracking branch 'origin/v8.5' into trunkHugo Herbelin
2015-09-08New option "Unset Bracketing Last Introduction Pattern" for preservingHugo Herbelin
2015-09-08Documenting the new behaviour of the Shrink Obligations flag.Pierre-Marie Pédrot
2015-08-22Documenting the Shrink Abstract option.Pierre-Marie Pédrot
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-08-02Granting Jason's request for an ad hoc compatibility option onHugo Herbelin
2015-08-02Documenting change of behavior of apply when the lemma is a tuple andHugo Herbelin
2015-07-10Rewording about how to upgrade on failing calls to constructor.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 18:53:54 +0000