diff options
Diffstat (limited to 'backend/CSE.v')
| -rw-r--r-- | backend/CSE.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 85f46e2..1888fb8 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -21,7 +21,6 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. |