Skip to content

Commit

Permalink
update changelog
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Jan 31, 2024
1 parent 6b98188 commit c8bff49
Showing 1 changed file with 17 additions and 2 deletions.
19 changes: 17 additions & 2 deletions Changelog.md
Original file line number Diff line number Diff line change
@@ -1,14 +1,29 @@
# Changelog

## [2.0.2] - 22/01/2024
## [2.0.2] - 01/02/2024

Requires Elpi 1.18.1 and Coq 8.19.
Requires Elpi 1.18.2 and Coq 8.19.

### API
- Fix `coq.elaborate-*` does not erase the type annotation of `Let`s (regression
introduced in 2.0.1). This fix may introduce differences in generated names
- Fix `coq.elaborate-*` are not affected anymore by printing options

### Commands
- Fix install the right initial parsing state (the one before any synterp action
is re-played)

### HOAS
- Fix evar instantiation loss when crossing the elpi/ltac border
- Fix encoding of "definitional classes" (`Class` with no record)
- Fix order of implicit arguments of `Record`

### Misc
- Change requiring `elpi` does not load primitive integers nor primitive floats

### Apps
- TC: avoid declaring options twice (could make vscoq2 fail)

## [2.0.1] - 29/12/2023

Requires Elpi 1.18.1 and Coq 8.19.
Expand Down

0 comments on commit c8bff49

Please sign in to comment.