diff options
Diffstat (limited to 'driver/Compiler.v')
| -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. |