From 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 12 Jan 2015 14:24:01 +0100
Subject: Update test for #3363 now that Require is forbidden inside modules.

---
 test-suite/bugs/opened/3363.v | 17 +----------------
 1 file changed, 1 insertion(+), 16 deletions(-)

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