From 4285f31a9bfe580b369cd29b3b5dcf4f83de7fac Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 29 Oct 2017 14:56:41 +0100
Subject: [PATCH] add disjointness change to changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d4c2af05..a3305d696 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,7 @@ Changes in Coq:
 
 * Rename some things and change notation:
   - The unit of a camera: `empty` -> `unit`, `∅` -> `ε`
+  - Disjointness: `⊥` -> `##`
   - A proof mode type class `IntoOp` -> `IsOp`
   - OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete`
   - OFE elements whose equality is discrete: `Timeless` -> `Discrete`
-- 
GitLab