From d74622e26bf30ef8e3de08b151e9e76fbb153186 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 28 Aug 2023 13:58:21 +0000
Subject: [PATCH] better wording

---
 docs/style_guide.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/style_guide.md b/docs/style_guide.md
index b87c18ccb..be89b0ae2 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -63,7 +63,7 @@ Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`,
 ### `Require`
 
 Never put `Require` in the middle of a file. All `Require` must be at the top.
-If you only want to *import* a certain module in some specific place, you can do something like
+If you only want to *import* a certain module in some specific place (for instance, in a `Section` or other `Module`), you can do something like:
 
 ```coq
 From lib Require component.
-- 
GitLab