aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
2020-01-27Merge PR #11415: Remove the CoqIDE "Revert all Buffers" command.Hugo Herbelin
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-22Move new entries in 8.11.0 changelog.Théo Zimmermann
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-20[mltop] Deprecate -load-ml options in anticipation of #11409Emilio Jesus Gallego Arias
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
2020-01-17Remove the CoqIDE "Revert all Buffers" command.Pierre-Marie Pédrot
2020-01-16Adding a changelog.Pierre-Marie Pédrot
2020-01-14Merge PR #11370: [zify] elim let in MLPierre-Marie Pédrot
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with deco...Hugo Herbelin
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...Kazuhiko Sakaguchi
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Add Set NativeCompute TimingJason Gross
2020-01-08Add changelog entry for native string extractionMaxime Dénès
2020-01-08Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rstSimonBoulier
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
2020-01-07Trailing implicit error: changelogSimonBoulier
2020-01-06[micromega] fix of bug #11191Frédéric Besson
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-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
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-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 15:14:45 +0000