aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-26
|\
| * Mention bug 3199 fix as a source of incompatibilities.Gravatar Matthieu Sozeau2015-10-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Documenting the option "Strict Universe Declaration" in CHANGES.Gravatar Pierre-Marie Pédrot2015-10-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\|
| * 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
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|\|
| * Explain new flags for native_compute in CHANGES.Gravatar Maxime Dénès2015-09-16
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Hugo Herbelin2015-09-09
|\|
| * New option "Unset Bracketing Last Introduction Pattern" for preservingGravatar Hugo Herbelin2015-09-08
* | Documenting the new behaviour of the Shrink Obligations flag.Gravatar Pierre-Marie Pédrot2015-09-08
* | Documenting the Shrink Abstract option.Gravatar Pierre-Marie Pédrot2015-08-22
|/
* 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
* Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749)Gravatar Guillaume Melquiond2015-02-15
* Document the issue with trivial inductive types. (Workaround for bug #3984)Gravatar Guillaume Melquiond2015-02-13
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
* Updating CHANGES (grammar, thanks to AS for pointing it out) +Gravatar Hugo Herbelin2015-01-24
* Typos, grammar, layout in CHANGES (continued).Gravatar Hugo Herbelin2015-01-23
* Typos, grammar, layout in CHANGES.Gravatar Hugo Herbelin2015-01-23
* Documenting the removal of coercions between sig, sigT, sig2,Gravatar Hugo Herbelin2015-01-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 06:46:41 +0000