aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2020-01-03coq_makefile: don't use CAMLPKGS when building cmxa of mllibGaëtan Gilbert
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...Pierre-Marie Pédrot
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
2019-12-21Merge PR #11311: Fix handling of recursive notations with custom entriesHugo Herbelin
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-18Merge PR #11263: [micromega] fix efficiency regressionMaxime Dénès
2019-12-17Merge PR #10762: Fix refine and eapply to mark shelved goals as non-resolvabl...Maxime Dénès
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-12-12restrict minimization to set to flexiblesGaëtan Gilbert
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-09Fixes #11254 (not requiring coqlib to be set to report about coqtop version).Hugo Herbelin
2019-12-06Make the string argument of `time` print correctlyJason Gross
2019-12-06Merge PR #11127: Added theorem Nat.bezout_comm.Hugo Herbelin
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-12-04Update doc/changelog/02-specification-language/11233-master+fix11231-missing-...Hugo Herbelin
2019-12-03Update doc/changelog/03-notations/11172-master+coercion-notation-interleaved-...Hugo Herbelin
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-03Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02Allow to override build date with SOURCE_DATE_EPOCHBernhard M. Wiedemann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-29Merge PR #10931: Add types of changes to changelog entries.Emilio Jesus Gallego Arias
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-28Update README and make-changelog tool following introduction of changelog types.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
2019-11-28Fix extension of changelog file.Théo Zimmermann
2019-11-27Merge PR #11187: Remove deprecated commands `AddPath`, `AddRecPath` and `DelP...Emilio Jesus Gallego Arias
2019-11-27Changelog entry for #11187.Théo Zimmermann
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation regress...Hugo Herbelin
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 20:14:03 +0000