aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* congruence fix: test-suite code and update CHANGESGravatar Matthieu Sozeau2016-07-05
* Mention more fixes in CHANGES before we release pl2.Gravatar Maxime Dénès2016-07-04
* Univs/CHANGES: #4097 and annotations on notationsGravatar Matthieu Sozeau2016-06-27
* Reporting about a few bug fixes (to be continued).Gravatar Hugo Herbelin2016-06-09
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* Mention problems with fix of #4582 in CHANGES.Gravatar Maxime Dénès2016-04-22
* Mention #4548 (fixed) in CHANGES.Gravatar Maxime Dénès2016-04-22
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* Add changelog for 8.5pl1 after the fact.Gravatar Maxime Dénès2016-04-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 19:59:01 +0000