Skip to content

Commit

Permalink
chore: add release notes for leanprover#2470 and leanprover#2480
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored and zerox committed Oct 22, 2023
1 parent 0bd15be commit 0916968
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions RELEASES.md
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,9 @@ v4.1.0

* The signature of `Lake.buildO` has changed, `args` has been split into `weakArgs` and `traceArgs`. `traceArgs` are included in the input trace and `weakArgs` are not. See Lake's [FFI example](src/lake/examples/ffi/lib/lakefile.lean) for a demonstration of how to adapt to this change.

v4.1.0
---------

* The signatures of `Lean.importModules`, `Lean.Elab.headerToImports`, and `Lean.Elab.parseImports`
have [changed](https://github.com/leanprover/lean4/pull/2480) from taking `List Import` to `Array Import`.

Expand Down

0 comments on commit 0916968

Please sign in to comment.