summaryrefslogtreecommitdiff
path: root/driver
diff options
context:
space:
mode:
Diffstat (limited to 'driver')
-rw-r--r--driver/Compiler.v3
1 files changed, 0 insertions, 3 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 37f7bc2..ed27f38 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -13,12 +13,9 @@
(** The whole compiler and its proof of semantic preservation *)
(** Libraries. *)
-Require Import Axioms.
Require Import Coqlib.
-Require Import Maps.
Require Import Errors.
Require Import AST.
-Require Import Values.
Require Import Smallstep.
(** Languages (syntax and semantics). *)
Require Csyntax.