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

CHANGELOG entry.

parent ca55de72
No related branches found
No related tags found
1 merge request!428Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`.
Pipeline #74816 passed
......@@ -8,6 +8,8 @@ API-breaking change is listed.
`difference_difference_r` and `difference_difference_r_L`.
- Let `set_solver` use `eauto` (instead of `idtac`) as its default solver.
- Add tactic `tc_solve` (this was `iSolveTC` in Iris).
- Let `f_equiv` to use `reflexivity` in a way similar to `f_equal`. That is,
let `f_equiv` solve goals and subgoals of the form `R x x`.
The following `sed` script should perform most of the renaming
(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