Initializers for global variables: compile-time evaluation of expressions done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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" [ "()" ].