From a78ce3e7858601a248d1577abacace26001af529 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Jan 2017 10:32:46 +0100
Subject: [PATCH] CHANGELOG: list things have been renamed

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d7eb3f468..95343a52b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,6 +23,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Renaming and moving things around: uPred and the rest of the base logic are in
   `base_logic`, while `program_logic` is for everything involving the general
   Iris notion of a language.
+* Renaming in prelude.list: Rename `prefix_of` -> `prefix` and `suffix_of` ->
+  `suffix` in lemma names, but keep notation ``l1 `prefix_of` l2`` and ``l1
+  `suffix_of` l2``.  `` l1 `sublist` l2`` becomes ``l1 `sublist_of` l2``. Rename
+  `contains` -> `submseteq` and change `` l1 `contains` l2`` to ``l1 ⊆+ l2``.
 * Slightly weaker notion of atomicity: an expression is atomic if it reduces in
   one step to something that does not reduce further.
 * Changed notation for embedding Coq assertions into Iris.  The new notation is
-- 
GitLab