diff --git a/CHANGELOG.md b/CHANGELOG.md index 452c08f5527715e16e2cdce9ff2311d151facc8c..9df10dca27e7825665ee55f4d878da95e8d9ec6a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 ```