Revert "Update test for #3363 now that Require is forbidden inside modules."

This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.

1 files changed, 16 insertions, 1 deletions

diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/3363.v
index 8307fdf506..800d89573c 100644
--- a/test-suite/bugs/opened/3363.v
+++ b/test-suite/bugs/opened/3363.v
@@ -1,4 +1,19 @@
-(** In this file, either both [Check]s should fail, or both should succeed. *)
+(** 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.