From b4e88c15da749b3edbd56cb70bf280a8e7bbfc3c Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Mon, 16 Jul 2018 14:04:29 -0700
Subject: Add test for repeated section with same name

---
 CHANGES                                    | 1 +
 doc/sphinx/language/gallina-extensions.rst | 3 ++-
 test-suite/bugs/closed/8081.v              | 4 ++++
 3 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/8081.v

diff --git a/CHANGES b/CHANGES
index d3f07889fe..95378c1c29 100644
--- a/CHANGES
+++ b/CHANGES
@@ -78,6 +78,7 @@ Vernacular Commands
 - The `Set SsrHave NoTCResolution` command no longer has special global
   scope. If you want the previous behavior, use `Global Set SsrHave
   NoTCResolution`.
+- Multiple sections with the same name are allowed.
 
 Coq binaries and process model
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index d9b2490452..394b928ada 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -781,7 +781,8 @@ Section :ref:`gallina-definitions`).
 
 .. cmd:: Section @ident
 
-   This command is used to open a section named `ident`.
+   This command is used to open a section named :token:`ident`.
+   Section names do not need to be unique.
 
 
 .. cmd:: End @ident
diff --git a/test-suite/bugs/closed/8081.v b/test-suite/bugs/closed/8081.v
new file mode 100644
index 0000000000..0f2501aaa8
--- /dev/null
+++ b/test-suite/bugs/closed/8081.v
@@ -0,0 +1,4 @@
+Section foo.
+End foo.
+Section foo.
+End foo.
-- 
cgit v1.2.3