diff --git a/library/standard/data/list/basic.lean b/library/standard/data/list/basic.lean
index 091123f29..7a4566f14 100644
--- a/library/standard/data/list/basic.lean
+++ b/library/standard/data/list/basic.lean
@@ -288,3 +288,5 @@ end
 
 -- declare global notation outside the section
 infixl `++` : 65 := concat
+
+end list
\ No newline at end of file
diff --git a/library/standard/data/nat/basic.lean b/library/standard/data/nat/basic.lean
index 900bf6ac6..e9c9eb191 100644
--- a/library/standard/data/nat/basic.lean
+++ b/library/standard/data/nat/basic.lean
@@ -415,3 +415,4 @@ discriminate
 -- add_rewrite mul_succ_left mul_succ_right
 -- add_rewrite mul_comm mul_assoc mul_left_comm
 -- add_rewrite mul_distr_right mul_distr_left
+end nat
\ No newline at end of file
diff --git a/library/standard/logic/classes/congr.lean b/library/standard/logic/classes/congr.lean
index 6f2446eaa..00303fdaf 100644
--- a/library/standard/logic/classes/congr.lean
+++ b/library/standard/logic/classes/congr.lean
@@ -137,3 +137,4 @@ calc
     ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
 
 -- TODO: add or_left_comm, and_right_comm, and_left_comm
+end congr
\ No newline at end of file