Skip to content
Snippets Groups Projects
Commit b8561191 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

CHANGELOG.

parent 9fddc01a
No related branches found
No related tags found
1 merge request!473Take advantage of new Coq features in Coq 8.15
Pipeline #81686 passed
...@@ -46,6 +46,10 @@ longer supported by this release. ...@@ -46,6 +46,10 @@ longer supported by this release.
intersection. (by Marijn van Wezel) intersection. (by Marijn van Wezel)
- Add lemmas `map_filter_or` and `map_filter_and` for the union and intersection - Add lemmas `map_filter_or` and `map_filter_and` for the union and intersection
of filters on maps. (by Marijn van Wezel) of filters on maps. (by Marijn van Wezel)
- Set `Hint Mode Equiv !`; this might need some type annotations for ambiguous
uses of `≡`.
- Set `intuition_solver ::= auto` (the default is `auto with *`) instead of
redeclaring `intuition`.
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment