From b0033bce67dab61cb564bcb60e86aad8f3255b48 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Mar 2020 19:32:55 +0100
Subject: [PATCH] Fix Coqdoc.

---
 theories/list.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index a77fca1a..8c50591c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -401,9 +401,8 @@ used by [positives_flatten]. *)
 Definition positives_unflatten (p : positive) : option (list positive) :=
   positives_unflatten_go p [] 1.
 
-
 (** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] 
-over integers, provided [n >= 0]. If n < 0, then the range is empty. **)
+over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
 Definition seqZ (m len: Z) : list Z :=
   (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
 Arguments seqZ : simpl never.
-- 
GitLab