From b7efc7bdc290bdc9efbde1bb040c7b65729e3341 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 May 2020 13:12:33 +0200
Subject: [PATCH] rename array_tools -> array; update CHANGELOG
---
CHANGELOG.md | 4 ++--
_CoqProject | 2 +-
theories/heap_lang/lib/{array_tools.v => array.v} | 0
3 files changed, 3 insertions(+), 3 deletions(-)
rename theories/heap_lang/lib/{array_tools.v => array.v} (100%)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index eadb54038..58ed3cc85 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,9 +23,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
**Changes in heap_lang:**
-* Added support for deallocation of locations.
+* Added support for deallocation of locations via the `Free` operation.
* Added a fraction to the heap_lang `array` assertion.
-* Added array_tools library for deallocating, copying and cloning arrays.
+* Added `lib.array` module for deallocating, copying and cloning arrays.
* Added the ghost state for "invariant locations" to `heapG`. This affects the
statement of `heap_adequacy`, which is now responsible for initializing the
"invariant locations" invariant.
diff --git a/_CoqProject b/_CoqProject
index 1619de757..156b00d69 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -124,7 +124,7 @@ theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
theories/heap_lang/lib/diverge.v
theories/heap_lang/lib/arith.v
-theories/heap_lang/lib/array_tools.v
+theories/heap_lang/lib/array.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
diff --git a/theories/heap_lang/lib/array_tools.v b/theories/heap_lang/lib/array.v
similarity index 100%
rename from theories/heap_lang/lib/array_tools.v
rename to theories/heap_lang/lib/array.v
--
GitLab