From 035aac9a723deb8cedf8a34d1f8f7bcdeea2c7e6 Mon Sep 17 00:00:00 2001
From: Fardale <fardale+git@crans.org>
Date: Wed, 23 Oct 2019 13:28:40 +0200
Subject: [PATCH] add invariant in CCDeque.ml

---
 src/data/CCDeque.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/data/CCDeque.ml b/src/data/CCDeque.ml
index 4c800e42..a19b91ed 100644
--- a/src/data/CCDeque.ml
+++ b/src/data/CCDeque.ml
@@ -17,7 +17,9 @@ type 'a node = {
 (** Linked list of cells.
 
     invariant: only the first and last cells are allowed to
-    be anything but [Three] (all the intermediate ones are [Three]) *)
+    be anything but [Three] (all the intermediate ones are [Three])
+    The first and last cell are [Zero] if and only if the
+    deque is empty *)
 
 type 'a t = {
   mutable cur : 'a node;