aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2019-11-26Make rapply handle all numbers of underscoresJason Gross
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21Update doc/changelog/02-specification-language/11132-master+fix-implicit-let-...Hugo Herbelin
2019-11-21Taking @Zimmi48's comment into accountCyril Cohen
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-19coq_makefile: support COQBIN with no ending /Gaëtan Gilbert
2019-11-19added changelog entryCyril Cohen
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-15Update doc/changelog/04-tactics/10998-zify-complements.rstKazuhiko Sakaguchi
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01Add warnings regarding the experimental nature of the vos feature in the doc.Pierre-Marie Pédrot
2019-11-01Changelog entryMaxime Dénès
2019-11-01docs: Add entry in changelogErik Martin-Dorel
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
2019-10-31changelog for #10985Gaëtan Gilbert
2019-10-30Implement the unsupported attribute error using the warning systemGaëtan Gilbert
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-29Show diffs in "Show Proof."Jim Fehrle
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-28Add support for Sorts in numeral notationsJason Gross
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-21docs(changelog): Address @gares' commentErik Martin-Dorel
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 18:33:52 +0000