aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Update CHANGES with inversion_sigma entryGravatar Jason Gross2017-06-30
* Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\
| * [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
* | Document cumulativity for inductive typesGravatar Amin Timany2017-06-16
|/
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
* Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\
| * mention 'make world' without 'byte' in CHANGES + 2 minor suggestionsGravatar Pierre Letouzey2017-06-01
* | 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