aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-05-22[coqchk] Fix #5030Pierre Roux
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-21Merge PR #12368: Print a newline at the end of timing tablesGaëtan Gilbert
2020-05-20Print a newline at the end of timing tablesJason Gross
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
2020-05-17Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ...Jason Gross
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-16Merge PR #12288: Prove that classical reals implement constructive reals.Michael Soegtrop
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ...Vincent Semeria
2020-05-15Changelog entries for #8855.Théo Zimmermann
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...Emilio Jesus Gallego Arias
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Adding changelog.Pierre-Marie Pédrot
2020-05-14Added change log.Hugo Herbelin
2020-05-14Add changelog for #12323.Hugo Herbelin
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
2020-05-13Adding change log for #8808.Hugo Herbelin
2020-05-13Added change log.Hugo Herbelin
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-13Document the changes regarding the order of command-line options.Théo Zimmermann
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
2020-05-12Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.leAnton Trunov
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-12fuse changelogs for #11249 and #12237Olivier Laurent
2020-05-11Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.Hugo Herbelin
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-05-10Change log for #12223.Hugo Herbelin
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09[doc] Add hexadecimal numeralsPierre Roux
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
2020-05-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
2020-05-08Merge PR #12068: Coqide completion: tentative fix for #11943Pierre-Marie Pédrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-07rename Bool.leb into Bool.le (same for ltb and compareb)Olivier Laurent
2020-05-07Adding change log for #12146.Hugo Herbelin
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 16:32:05 +0000