diff options
Diffstat (limited to 'backend/RRE.v')
-rw-r--r-- | backend/RRE.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/backend/RRE.v b/backend/RRE.v index 95eadce..ece6051 100644 --- a/backend/RRE.v +++ b/backend/RRE.v @@ -13,10 +13,7 @@ (** Redundant Reloads Elimination *) Require Import Coqlib. -Require Import Maps. Require Import AST. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Conventions. |