diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index a285aa8d6fb7bbdf3212e3f79c0fa6efa8f8ffef..9928a2ca67674c7c348969c6a77ecb8c46da26f3 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.