diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-11-27 15:34:34 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-11-27 15:34:34 +0100 |
| commit | 3af2dc7aaa8c8139ddd26589258f2b289425f591 (patch) | |
| tree | e9c5d9912a91f51a80ae462c499e63c2f9ccc650 /driver | |
| parent | 5631ccb7c416bb7ecbe7920cb432a78436c0a7ac (diff) | |
| download | compcert-kvx-3af2dc7aaa8c8139ddd26589258f2b289425f591.tar.gz compcert-kvx-3af2dc7aaa8c8139ddd26589258f2b289425f591.zip | |
Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..6d398327 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -69,7 +69,7 @@ Require Linearizeproof. Require CleanupLabelsproof. Require Debugvarproof. Require Stackingproof. -Require Asmgenproof. +Require Import Asmgenproof. (** Command-line flags. *) Require Import Compopts. |