summaryrefslogtreecommitdiff
path: root/common/Smallstep.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Smallstep.v')
-rw-r--r--common/Smallstep.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 458e8c6..02b18fc 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -22,7 +22,6 @@
Require Import Relations.
Require Import Wellfounded.
Require Import Coqlib.
-Require Import AST.
Require Import Events.
Require Import Globalenvs.
Require Import Integers.