summaryrefslogtreecommitdiff
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 1689ad2..5fc6795 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -10,13 +10,13 @@
(* *)
(* *********************************************************************)
-Require List.
Require Iteration.
Require Floats.
Require RTLgen.
Require Coloring.
Require Allocation.
Require Compiler.
+Require Initializers.
(* Standard lib *)
Extract Inductive unit => "unit" [ "()" ].