aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2016-01-12Reporting about the new tactical unshelve.Hugo Herbelin
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-14Updating CHANGES with an incompatibility.Hugo Herbelin
2015-12-14Flag -compat 8.4 now loads Coq.Compat.Coq84.Maxime Dénès
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-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-05Fix CHANGES.Hugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-12Update CHANGESJason Gross
2015-11-11Fix bug #3735: interpretation of "->" in Program follows the standard one.Matthieu Sozeau
2015-11-05Update version numbers and magic numbers for 8.5beta3 release.Maxime Dénès
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-21Mention bug 3199 fix as a source of incompatibilities.Matthieu Sozeau
2015-10-19Documenting the option "Strict Universe Declaration" in CHANGES.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
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-16Explain new flags for native_compute in CHANGES.Maxime Dénès
2015-09-08New option "Unset Bracketing Last Introduction Pattern" for preservingHugo Herbelin
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
2015-07-10CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla.Maxime Dénès
2015-07-05More precise rewording about asymmetric patterns.Hugo Herbelin
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-18Fixed CHANGES to reflect -color option.Pierre Courtieu
2015-05-14Adding an option -w to control Coq warning output.Pierre-Marie Pédrot
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-13Documenting the Loose Hint Behavior flag.Pierre-Marie Pédrot
2015-05-09Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forHugo Herbelin
2015-05-04Fix documentation of RedirectEnrico Tassi
2015-04-22More precise numbers about Benjamin's fix for the VM.Maxime Dénès
2015-04-22Update CHANGESMatthieu Sozeau
2015-04-07Removing references to -I -as from CHANGES.Pierre-Marie Pédrot
2015-04-01Accomodating #4166 (providing "Require Import OmegaTactic" as aHugo Herbelin
2015-03-22Announcing * and ** which were not official yet in 8.4.Hugo Herbelin
2015-03-22Aliasing give_up with admitEnrico Tassi
2015-03-13CHANGES: more correct equivalent to "constructor tac" syntax.Arnaud Spiwack
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-28Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ...Pierre Boutillier
2015-02-24CHANGES: Info command + info_auto currently broken.Arnaud Spiwack
2015-02-15Undo: back to 8.4 semantics (Close #3514)Enrico Tassi
2015-02-15Note about "Undo. Undo." in CHANGESEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:23:21 +0000