Add test for repeated section with same name

1 files changed, 1 insertions, 0 deletions

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