From 29c117af02bc2fa30866a4b2dc933e57b0d68f2a Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 25 Feb 2019 14:24:14 +0100
Subject: [PATCH] clarify that modalities can be heterogeneous

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

diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index e47b99797..9b84c16df 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -7,9 +7,9 @@ Import bi.
 instantiated with a variety of modalities.
 
 For the purpose of MoSeL, a modality is a mapping of propositions
-`M : PROP → PROP` (where `PROP` is a type of bi-assertions) that is
-monotone and distributes over finite products. Specifically, the following
-rules have to be satisfied.
+`M : PROP1 → PROP2` (where `PROP1` and `PROP2` are BI-algebras)
+that is monotone and distributes over finite products. Specifically,
+the following rules have to be satisfied:
 
       P ⊢ Q        emp ⊢ M emp
     ----------
-- 
GitLab