From a4d6d9131d724107c04f0d9865dde0b8361a7304 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 22 Apr 2020 17:34:50 +0200
Subject: [PATCH] Fix some typos in docs

---
 theories/proofmode/classes.v     | 2 +-
 theories/proofmode/coq_tactics.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index d9603ff41..daa46a7c9 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 daea5a760..6b8eb48ea 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.
-- 
GitLab