aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\
| * Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
* | Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
|/
* Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \
| * | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
* | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
|/ /
| * Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
|/
* Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\
* | Aligning on standard layout of CHANGES.Gravatar Hugo Herbelin2017-05-13
| * Documenting Printing Compact Contexts + CHANGESGravatar Pierre Courtieu2017-05-11
* | Tentative note in CHANGES about now applying βι while typing "match" branches.Gravatar Hugo Herbelin2017-04-27
|/
* CHANGES entry for #545.Gravatar Maxime Dénès2017-04-19
* Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\
| * Documenting the changes introduced by the EConstr branch.Gravatar Pierre-Marie Pédrot2017-04-10
* | [camlpX] Enrico's changes to camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
|/
* Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\
* | Document the changes to IZR.Gravatar Guillaume Melquiond2017-03-22
| * Farewell decl_modeGravatar Enrico Tassi2017-03-07
* | CHANGES: choice over setoids and prop. ext.Gravatar Hugo Herbelin2017-03-03
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\
| * A few words in CHANGES.Gravatar Maxime Dénès2016-12-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * [doc] Mention XML protocol on changes.Gravatar Emilio Jesus Gallego Arias2016-11-16
| * Remove the list of bug fixes from CHANGES.Gravatar Maxime Dénès2016-11-14
| * Update CHANGES and credits for 8.6beta1.Gravatar Maxime Dénès2016-11-10
| * Mention notypeclasses refine in CHANGESGravatar Matthieu Sozeau2016-11-07
| * CHANGES for this branch.Gravatar Matthieu Sozeau2016-11-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\
| | * Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Gravatar Maxime Dénès2016-10-25
| | * Update CHANGES.Gravatar Maxime Dénès2016-10-25
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
* | | Allocating a section in CHANGES for changes specific to 8.7.Gravatar Hugo Herbelin2016-10-12
| * | Tentatively preparing to add changes specific to v8.7 (see PR #275).Gravatar Hugo Herbelin2016-10-12
|/ /
* | Report about changes of semantics of auto as an ltac argument (see #4966).Gravatar Hugo Herbelin2016-10-08
* | Remove the Set Verbose Compat option and turn the warning on by default.Gravatar Maxime Dénès2016-10-06
* | Document change related to Keep Proof Equalities in CHANGES.Gravatar Maxime Dénès2016-10-03
* | Being more informative about the change of behavior of "subst".Gravatar Hugo Herbelin2016-09-29
* | Fix description of change in intro semantics.Gravatar Maxime Dénès2016-09-21
* | Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\|
| * Fixing CHANGES.Gravatar Hugo Herbelin2016-08-17
* | Documenting fix of #3070 (subst and chain of dependencies).Gravatar Hugo Herbelin2016-08-17
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\|
| * Fix #5000: Document the native compiler soundness bug due to Unicode mangling.Gravatar Pierre-Marie Pédrot2016-08-07
| * Fix bug #4673: regression in setoid_rewrite.Gravatar Matthieu Sozeau2016-07-29