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

CHANGELOG entry.

parent 360e1cf4
Branches
Tags
No related merge requests found
......@@ -29,6 +29,10 @@ Coq 8.13 is no longer supported.
not dispose of hypotheses to perform the rewrite.
* Remove tactic `iSolveTC` in favor of `tc_solve` in std++.
**Changes in `heap_lang`:**
* Move operations and lemmas about locations into a module `Loc`.
**LaTeX changes:**
- Rename `\Alloc` to `\AllocN` and `\Ref` to `\Alloc` for better consistency
......@@ -44,6 +48,9 @@ s/iSolveTC\b/tc_solve/g
# _alt -> _def
s/\bsig_equiv_alt\b/sig_equiv_def/g
s/\bsig_dist_alt\b/sig_dist_def/g
# Loc
s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g
s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
EOF
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment