aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-29Merge PR #10947: Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in `...Enrico Tassi
2019-10-28Merge PR #10963: Possible simplification of parsing rules.Clément Pit-Claudel
2019-10-28Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile`...Kazuhiko Sakaguchi
2019-10-28Fix typos.Théo Zimmermann
2019-10-28Add changelog for #10963.Théo Zimmermann
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-10-24Release notes for Coq 8.10.1Vincent Laporte
2019-10-22Update doc/changelog/06-ssreflect/10932-void-type-ssr.rst Arthur Azevedo de Amorim
2019-10-22Update changelog.Arthur Azevedo de Amorim
2019-10-21Adding changelogHugo Herbelin
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ...Gaëtan Gilbert
2019-10-18Merge PR #10895: Logic: Add equivalence between weak excluded-middle and clas...Pierre-Marie Pédrot
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
2019-10-15Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.Clément Pit-Claudel
2019-10-14Updating changelogHugo Herbelin
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
2019-10-11Document Gaëtan's new script to prefill a changelog entry.Théo Zimmermann
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-05Changelog for SProp onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive projec...Frédéric Besson
2019-10-03fix 10765-micromega-caches.rstFrédéric Besson
2019-10-03Improved handling of micromega cachesFrédéric Besson
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-24Merge PR #10774: Make `zify` does work for `Z.to_N`Frédéric Besson
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
2019-09-17Add changelog entryMaxime Dénès
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-09-16Re-implementation of zifyFrédéric Besson
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
2019-09-05Merge PR #10731: Ocfnash/stdlib additionsHugo Herbelin
2019-09-04Add changelog entry for 10731Oliver Nash
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-03Apply suggestions from code reviewOliver Nash
2019-09-03New lemmas for List.vOliver Nash
2019-09-01edits per reviewYishuai Li
2019-09-01Changelog: more accurate on unconsYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-09Add a changelog entryKazuhiko Sakaguchi
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-10 20:46:43 +0000