From 6b1af5f32ee1d7ee444f09c5904b637bee65e5d2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Feb 2018 16:47:20 +0100
Subject: [PATCH] Comment about `FromModal`.

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

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index a285aa8d6..9928a2ca6 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -229,6 +229,10 @@ Section modality1.
   Qed.
 End modality1.
 
+(** The [FromModal M P Q] class is used by the [iModIntro] tactic to transform
+a goal [P] into a modality [M] and proposition [Q].
+
+The input is [P] and the outputs are [M] and [Q]. *)
 Class FromModal {PROP1 PROP2 : bi}
     (M : modality PROP1 PROP2) (P : PROP2) (Q : PROP1) :=
   from_modal : M Q ⊢ P.
-- 
GitLab