From e13f0bb3391177bb614d26d07383c94b96d0bf4c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 17 Jan 2015 09:43:54 +0100
Subject: Revert "Update test for #3363 now that Require is forbidden inside
 modules."

This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
---
 test-suite/bugs/opened/3363.v | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

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.
-- 
cgit v1.2.3