aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblockgenproof0.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Asmblockgenproof0.v')
-rw-r--r--aarch64/Asmblockgenproof0.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 4217f526..03d863a3 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -37,7 +37,6 @@ Require Import Asmblock.
Require Import Asmblockgen.
Require Import Conventions1.
Require Import Axioms.
-Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
Require Import Asmblockprops.
Module MB:=Machblock.