aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
* 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
* 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
* 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
* Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
* Fix CHANGES.Gravatar Hugo Herbelin2015-12-05
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Update CHANGESGravatar Jason Gross2015-11-12
* Fix bug #3735: interpretation of "->" in Program follows the standard one.Gravatar Matthieu Sozeau2015-11-11
* Update version numbers and magic numbers for 8.5beta3 release.Gravatar Maxime Dénès2015-11-05
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* Mention bug 3199 fix as a source of incompatibilities.Gravatar Matthieu Sozeau2015-10-21
* Documenting the option "Strict Universe Declaration" in CHANGES.Gravatar Pierre-Marie Pédrot2015-10-19
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
* Explain new flags for native_compute in CHANGES.Gravatar Maxime Dénès2015-09-16
* New option "Unset Bracketing Last Introduction Pattern" for preservingGravatar Hugo Herbelin2015-09-08
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* Documenting change of behavior of apply when the lemma is a tuple andGravatar Hugo Herbelin2015-08-02
* Rewording about how to upgrade on failing calls to constructor.Gravatar Hugo Herbelin2015-07-10
* CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla.Gravatar Maxime Dénès2015-07-10
* More precise rewording about asymmetric patterns.Gravatar Hugo Herbelin2015-07-05
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Fixed CHANGES to reflect -color option.Gravatar Pierre Courtieu2015-05-18
* Adding an option -w to control Coq warning output.Gravatar Pierre-Marie Pédrot2015-05-14
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Documenting the Loose Hint Behavior flag.Gravatar Pierre-Marie Pédrot2015-05-13
* Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forGravatar Hugo Herbelin2015-05-09
* Fix documentation of RedirectGravatar Enrico Tassi2015-05-04
* More precise numbers about Benjamin's fix for the VM.Gravatar Maxime Dénès2015-04-22
* Update CHANGESGravatar Matthieu Sozeau2015-04-22
* Removing references to -I -as from CHANGES.Gravatar Pierre-Marie Pédrot2015-04-07
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
* Announcing * and ** which were not official yet in 8.4.Gravatar Hugo Herbelin2015-03-22
* Aliasing give_up with admitGravatar Enrico Tassi2015-03-22
* CHANGES: more correct equivalent to "constructor tac" syntax.Gravatar Arnaud Spiwack2015-03-13
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ...Gravatar Pierre Boutillier2015-02-28
* CHANGES: Info command + info_auto currently broken.Gravatar Arnaud Spiwack2015-02-24
* Undo: back to 8.4 semantics (Close #3514)Gravatar Enrico Tassi2015-02-15
* Note about "Undo. Undo." in CHANGESGravatar Enrico Tassi2015-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:48:53 +0000