aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
2021-04-22Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function.coqbot-app[bot]
2021-04-22Add changelogPierre Roux
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
2021-04-19changelog entry for Ltac2 unifySamuel Gruetter
2021-04-17Uniformize the name of the Ltac2 boolean equality function.Pierre-Marie Pédrot
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
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-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
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-30Remove the :> type castJim Fehrle
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:35:48 +0000