From acd4bf1532305f84f8365ae4310101910ee44504 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Aug 2023 14:23:26 +0200
Subject: [PATCH] never put Require in the middle of a file

---
 docs/style_guide.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/docs/style_guide.md b/docs/style_guide.md
index c09039634..b87c18ccb 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -60,6 +60,19 @@ Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`,
 
 **TODO:** Always add `Global` or `Local` to `Hint`, `Arguments`, and `Instance`.
 
+### `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
+
+```coq
+From lib Require component.
+
+(* ... *)
+
+Import component.
+```
+
 ### Ltac
 
 We prefer `first [ t1 | fail 1 "..." ]` to `t1 || fail "..."` because the latter will fail if `t1` doesn't make progress. See https://gitlab.mpi-sws.org/iris/iris/-/issues/216. Note that `first [ t1 | fail "..."]` is simply incorrect; the failure message will never show up and will be replaced with a generic failure.
-- 
GitLab