From bb39a0238ac341c407aef9ca8e8601c75789d3b5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 4 Nov 2019 16:46:55 +0100
Subject: Forbid Include inside sections

This probably does not work well in general, and specifically avoids
an anomaly fixing https://github.com/coq/coq/issues/10060
---
 test-suite/bugs/closed/bug_10060.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10060.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/bug_10060.v b/test-suite/bugs/closed/bug_10060.v
new file mode 100644
index 0000000000..d74f6e388b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10060.v
@@ -0,0 +1,15 @@
+Module Type T.
+  Parameter b : Set.
+End T.
+
+Module M1(N : T).
+End M1.
+
+Module M2.
+End M2.
+
+Section S.
+  Variable a : Set.
+  Definition b := a.
+  Fail Include M1.
+End S.
-- 
cgit v1.2.3