From 495962d5aa69e30a64ad8a2b3b8fe2184e3b515c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Mar 2018 11:45:57 +0100
Subject: [PATCH] Improve comment.

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

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 09217c4f8..275e6c686 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -89,10 +89,10 @@ a goal [P] into a modality [M] and proposition [Q].
 
 The input is [P] and the outputs are [M] and [Q].
 
-For modalities [M] that do not need to augment the proof mode environment, one
-can define an instance [FromModal modality_id (M P) P]. Defining such an
-only imposes the proof obligation [P ⊢ M P]. Examples of modalities that have
-such an instance are [bupd], [fupd], [except_0], [monPred_relatively] and
+For modalities [N] that do not need to augment the proof mode environment, one
+can define an instance [FromModal modality_id (N P) P]. Defining such an
+instance only imposes the proof obligation [P ⊢ N P]. Examples of such
+modalities [N] are [bupd], [fupd], [except_0], [monPred_relatively] and
 [bi_absorbingly]. *)
 Class FromModal {PROP1 PROP2 : bi}
     (M : modality PROP1 PROP2) (P : PROP2) (Q : PROP1) :=
-- 
GitLab