From 20f9a1404f84ddabde2d1cbacc9063d9de87dfa9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 17 Jan 2015 09:44:44 +0100
Subject: Revert "Adapting two files from test-suite to now forbidden Require's
 in modules."

This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e.
---
 test-suite/bugs/closed/2830.v | 4 ++--
 test-suite/bugs/closed/3188.v | 6 ++----
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v
index 219838aa3a..b72c821dfd 100644
--- a/test-suite/bugs/closed/2830.v
+++ b/test-suite/bugs/closed/2830.v
@@ -39,10 +39,10 @@ End A.
 
 (* 2- This was submitted by Andrew Appel *)
 
-Require Import Program Relations.
-
 Module B.
 
+Require Import Program Relations.
+
 Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A)  :=
 { af_unage : forall x x' y', level x' = level y' -> age1 x = Some x' -> exists y, age1 y = Some y'
 ; af_level1 : forall x, age1 x = None <-> level x = 0
diff --git a/test-suite/bugs/closed/3188.v b/test-suite/bugs/closed/3188.v
index 09ab4ca583..0117602670 100644
--- a/test-suite/bugs/closed/3188.v
+++ b/test-suite/bugs/closed/3188.v
@@ -1,8 +1,7 @@
 (* File reduced by coq-bug-finder from 1656 lines to 221 lines to 26 lines to 7 lines. *)
 
-Require Import Coq.Classes.RelationClasses.
-
 Module Long.
+  Require Import Coq.Classes.RelationClasses.
 
   Hint Extern 0 => apply reflexivity : typeclass_instances.
   Hint Extern 1 => symmetry.
@@ -12,9 +11,8 @@ Module Long.
   Abort.
 End Long.
 
-Require Import Coq.Classes.RelationClasses.
-
 Module Short.
+  Require Import Coq.Classes.RelationClasses.
 
   Hint Extern 0 => apply reflexivity : typeclass_instances.
 
-- 
cgit v1.2.3