Fix some typos in docs

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].

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.