diff options
Diffstat (limited to 'backend/SplitLong.vp')
| -rw-r--r-- | backend/SplitLong.vp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 694bb0e2..73e22b98 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -16,6 +16,7 @@ Require String. Require Import Coqlib. Require Import AST Integers Floats. Require Import Op CminorSel. +Require Import OpHelpers. Require Import SelectOp. Local Open Scope cminorsel_scope. |