aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
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-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
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
2019-07-29Document changes by PR 10324Vincent Laporte
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
2019-07-18Shorten changelogVincent Semeria
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
2019-07-08Adding a changelog.Pierre-Marie Pédrot
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-13Add missing changelog entry for #10360.Théo Zimmermann
2019-06-12Merge PR #10329: Update changelog for 10302 and 10305Théo Zimmermann
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the v...Emilio Jesus Gallego Arias
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-08Updated changelog.Hugo Herbelin
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
2019-06-07Update changelog for 103032 and 10305Enrico Tassi
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-06-04Fix typo in changelogEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:10:20 +0000