From 9f23a5ce127b25169e46167a8294cbb2cb6ef2e1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Feb 2023 20:08:40 +0100
Subject: [PATCH] CHANGELOG entry.

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 452c08f55..9df10dca2 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
 ```
 
-- 
GitLab