diff options
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 96162f9e..ddd58223 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -36,6 +36,7 @@ Require Import Values Memory Events Globalenvs Smallstep. Require Import Locations Conventions. Require Stacklayout. Require Import OptionMonad Asm. +Require Export Asm. Local Open Scope option_monad_scope. |