diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Compiler.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 37f7bc2d..ed27f383 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. |