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