1 files changed, 6 insertions, 7 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index f466a90..83e82e1 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -18,6 +18,12 @@ Require Import Maps.
 Require Import AST.
 Require Import Op.
 Require Import Registers.
+Require Import Globalenvs.
+Require Import Values.
+Require Import Mem.
+Require Import Integers.
+Require Import Events.
+Require Import Smallstep.
 Require Import RTL.
 Require Conventions.
 
@@ -398,13 +404,6 @@ Qed.
   here, as a warm-up exercise and because some of the lemmas will be
   useful later. *)
 
-Require Import Globalenvs.
-Require Import Values.
-Require Import Mem.
-Require Import Integers.
-Require Import Events.
-Require Import Smallstep.
-
 Definition wt_regset (env: regenv) (rs: regset) : Prop :=
   forall r, Val.has_type (rs#r) (env r).