Skip to content

Commit 72c39ec

Browse files
committed
chore: add release notes for #2470 and #2480
1 parent be97757 commit 72c39ec

File tree

1 file changed

+13
-0
lines changed

1 file changed

+13
-0
lines changed

RELEASES.md

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,19 @@ only an expectation that breaking changes will be documented in this file.
77
This file contains work-in-progress notes for the upcoming release, as well as previous stable releases.
88
Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status of each version.
99

10+
v4.1.0
11+
---------
12+
13+
* The signatures of `Lean.importModules`, `Lean.Elab.headerToImports`, and `Lean.Elab.parseImports`
14+
have [changed](https://github.com/leanprover/lean4/pull/2480) from taking `List Import` to `Array Import`.
15+
16+
* There is now [an `occs` field](https://github.com/leanprover/lean4/pull/2470)
17+
in the configuration object for the `rewrite` tactic,
18+
allowing control of which occurrences of a pattern should be rewritten.
19+
This was previously a separate argument for `Lean.MVarId.rewrite`,
20+
and this has been removed in favour of an additional field of `Rewrite.Config`.
21+
It was not previously accessible from user tactics.
22+
1023
v4.0.0
1124
---------
1225

0 commit comments

Comments
 (0)