Skip to content
Snippets Groups Projects
Commit f09470bb authored by Ralf Jung's avatar Ralf Jung
Browse files

changelog

parent 928684f9
No related branches found
No related tags found
1 merge request!289add mk_evar tactic (to replace Coq's strange evar tactic) and use it
Pipeline #50424 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
CHANGELOG.md
+ 2
− 0
View file @ f09470bb
...@@ -109,6 +109,8 @@ API-breaking change is listed. ...@@ -109,6 +109,8 @@ API-breaking change is listed.
is consistent with `delete_insert`. is consistent with `delete_insert`.
- Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso) - Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
- Make `done` work on goals of the form `is_Some`. - Make `done` work on goals of the form `is_Some`.
- Add `mk_evar` tactic to generate evars (intended as a more useful replacement
for Coq's `evar` tactic).
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% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment