summaryrefslogtreecommitdiff
path: root/common/Behaviors.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Behaviors.v')
-rw-r--r--common/Behaviors.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 454ea34..0a7ed17 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -18,7 +18,6 @@
Require Import Classical.
Require Import ClassicalEpsilon.
Require Import Coqlib.
-Require Import AST.
Require Import Events.
Require Import Globalenvs.
Require Import Integers.