aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2021-04-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
2021-04-19changelog entry for Ltac2 unifySamuel Gruetter
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-04-12[coqdep] error on non-existent and unreadable filesHendrik Tews
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
2021-04-04Adding change log for #13624.Hugo Herbelin
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
2021-03-30Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.Michael Soegtrop
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies:...coqbot-app[bot]
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-26Document as critical.Guillaume Melquiond
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
2021-03-26Adding a changelog.Pierre-Marie Pédrot
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
2021-03-26Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmascoqbot-app[bot]
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to...coqbot-app[bot]
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map,...Andrej Dudenhefner
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
2021-03-16correct changelog #13582Olivier Laurent
2021-03-16add changelogOlivier Laurent
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-13Documenting the changes.Pierre-Marie Pédrot
2021-03-13Minimize the set of multiple inheritance paths to check for conversionKazuhiko Sakaguchi
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Adding documentation of the changes.Pierre-Marie Pédrot
2021-03-09Add changelogKazuhiko Sakaguchi
2021-03-06[vernac] Improve alpha-renaming in record projection typesLi-yao Xia
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04[doc] changelog entryEnrico Tassi
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-28Merge PR #13853: Delay the dynamic linking of native-code libraries until nat...Pierre-Marie Pédrot
2021-02-27Merge PR #13876: [coqc] Don't allow to pass more than one file to coqccoqbot-app[bot]
2021-02-27Add changelogPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 10:55:49 +0000