aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Compiler.v
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Compiler.v')
-rw-r--r--driver/Compiler.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v
index cbf7df87..1580fcd6 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -13,6 +13,7 @@
(** The whole compiler and its proof of semantic preservation *)
(** Libraries. *)
+Require Import Axioms.
Require Import Coqlib.
Require Import Maps.
Require Import Errors.