diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index d9603ff412841d81aeb129c68a314f3285f4287b..daa46a7c92e584bb89591f89fef3df1c9e27cd85 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -91,7 +91,7 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-(** The [FromModal M P Q] class is used by the [iModIntro] tactic to transform
+(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to transform
 a goal [P] into a modality [M] and proposition [Q].
 
 The inputs are [P] and [sel] and the outputs are [M] and [Q].
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index daea5a76008dad4940a9075262a88454c4fd101b..6b8eb48ea5bd14527b81e12758fc08832d1725d2 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -818,8 +818,8 @@ Class TransformIntuitionisticEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
   transform_intuitionistic_env_dom i : Γin !! i = None → Γout !! i = None;
 }.
 
-(* The class [TransformIntuitionisticEnv M C Γin Γout filtered] is used to transform
-the intuitionistic environment using a type class [C].
+(* The class [TransformSpatialEnv M C Γin Γout filtered] is used to transform
+the spatial environment using a type class [C].
 
 Inputs:
 - [Γin] : the original environment.