aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* All arguments defined through ARGUMENT EXTEND declare a tactic scope.Gravatar Pierre-Marie Pédrot2016-03-04
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
* Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\
| * Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
| * Fix CHANGES.Gravatar Hugo Herbelin2015-12-05
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
| * Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-15
|\|
| * Update CHANGESGravatar Jason Gross2015-11-12
| * Fix bug #3735: interpretation of "->" in Program follows the standard one.Gravatar Matthieu Sozeau2015-11-11
* | Listing separately changes from 8.5betas to final 8.5 and furtherGravatar Hugo Herbelin2015-11-10
* | Activating bracketing of last or-and introduction pattern by defaultGravatar Hugo Herbelin2015-11-10
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * 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
* | 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