1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/3363.v
new file mode 100644
index 00000000..800d8957
--- /dev/null
+++ b/test-suite/bugs/opened/3363.v
@@ -0,0 +1,26 @@
+(** In this file, either all four [Check]s should fail, or all four should succeed. *)
+Module A.
+  Section HexStrings.
+    Require Import String.
+  End HexStrings.
+  Fail Check string.
+End A.
+
+Module B.
+  Section HexStrings.
+    Require String.
+    Import String.
+  End HexStrings.
+  Fail Check string.
+End B.
+
+Section HexStrings.
+  Require String.
+  Import String.
+End HexStrings.
+Fail Check string.
+
+Section HexStrings'.
+  Require Import String.
+End HexStrings'.
+Check string.