From 336a8c7d3e946a5d2d959970cbced9b988eaa6b7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Feb 2019 17:28:32 +0100
Subject: [PATCH] Tweak modalities doc.

---
 theories/proofmode/modalities.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index 36e54a347..b5b9bcc0a 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -8,8 +8,8 @@ instantiated with a variety of modalities.
 
 For the purpose of MoSeL, a modality is a mapping of propositions
 `M : PROP1 → PROP2` (where `PROP1` and `PROP2` are BI-algebras, although usually
-it is the same algebra) that is monotone and distributes over finite products.
-Specifically, the following rules have to be satisfied:
+it is the same algebra) that is monotone and distributes over separating
+conjunction. Specifically, the following rules have to be satisfied:
 
       P ⊢ Q        emp ⊢ M emp
     ----------
-- 
GitLab