aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Collapse)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-04-22Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-22Add changelogPierre Roux
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
Reviewed-by: JasonGross Ack-by: jfehrle
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Zimmi48
2021-04-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-04-19changelog entry for Ltac2 unifySamuel Gruetter
2021-04-17Uniformize the name of the Ltac2 boolean equality function.Pierre-Marie Pédrot
All other equality functions are called "equal" but this one was called "eq". We add a deprecated alias for backward compatibility.
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence.
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-12[coqdep] error on non-existent and unreadable filesHendrik Tews
Print an error message and return non-zero status for non-existing or unreadable files. Unknown options produce a warning and are otherwise ignored. Fixes #14023
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
Fixes #14092: Print Grammar ltac2 should exist.
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
Reviewed-by: olaure01 Ack-by: jfehrle
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: silene Ack-by: SkySkimmer Ack-by: olaure01
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
add polynomial specifications of to_nat add changelog and doc entries
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
The old code was generating different patterns, depending on whether a projection with parameters was expanded or not. In the first case, parameters were present, whereas in the latter they were not. We fix this by adding dummy parameter arguments on sight. Fixes #14009: TC search failure with primitive projections.
2021-03-30Remove the :> type castJim Fehrle
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-30Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary ↵coqbot-app[bot]
dependencies: Le, Gt, Minus, Lt, Setoid Reviewed-by: anton-trunov
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
Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011
2021-03-26Adding a changelog.Pierre-Marie Pédrot
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
fix unexpectedly broken MSetGenTree.v add changelog entry
2021-03-26Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmascoqbot-app[bot]
Reviewed-by: olaure01
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths ↵coqbot-app[bot]
to check for conversion Reviewed-by: gares Ack-by: SkySkimmer
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, ↵Andrej Dudenhefner
Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
Reviewed-by: anton-trunov
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
The table of coercion classes (`class_tab`) has been extended with information about reachability. The conversion checking of a pair of multiple inheritance paths (of coercions) will be skipped if these paths can be reduced to smaller adjoining pairs of multiple inheritance paths, and this reduction will be determined based on that reachability information.
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: jfehrle
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
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:03:58 +0000