Reorganized the development, modularizing away machine-dependent parts.

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


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

4 files changed, 26 insertions, 646 deletions

diff --git a/extraction/.depend b/extraction/.depend
deleted file mode 100644
index a8ae227..0000000
--- a/extraction/.depend
+++ /dev/null
@@ -1,529 +0,0 @@
-../caml/CMlexer.cmi: ../caml/CMparser.cmi 
-../caml/CMparser.cmi: Cminor.cmi AST.cmi 
-../caml/CMtypecheck.cmi: Cminor.cmi 
-../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \
-    InterfGraph.cmi 
-../caml/PrintPPC.cmi: PPC.cmi 
-../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CString.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi 
-../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CString.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx Ascii.cmx 
-../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
-    CList.cmi AST.cmi 
-../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
-    CList.cmx AST.cmx 
-../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \
-    ../caml/CMlexer.cmi 
-../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \
-    ../caml/CMlexer.cmi 
-../caml/CMparser.cmo: Integers.cmi Datatypes.cmi Cminor.cmi \
-    ../caml/Camlcoq.cmo CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
-    ../caml/CMparser.cmi 
-../caml/CMparser.cmx: Integers.cmx Datatypes.cmx Cminor.cmx \
-    ../caml/Camlcoq.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
-    ../caml/CMparser.cmi 
-../caml/CMtypecheck.cmo: Integers.cmi Datatypes.cmi Cminor.cmi \
-    ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/CMtypecheck.cmi 
-../caml/CMtypecheck.cmx: Integers.cmx Datatypes.cmx Cminor.cmx \
-    ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/CMtypecheck.cmi 
-../caml/Coloringaux.cmo: Registers.cmi RTLtyping.cmi RTL.cmi Maps.cmi \
-    Locations.cmi InterfGraph.cmi Datatypes.cmi Conventions.cmi \
-    ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi ../caml/Coloringaux.cmi 
-../caml/Coloringaux.cmx: Registers.cmx RTLtyping.cmx RTL.cmx Maps.cmx \
-    Locations.cmx InterfGraph.cmx Datatypes.cmx Conventions.cmx \
-    ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi 
-../caml/Driver.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \
-    Errors.cmi Csyntax.cmi ../caml/Configuration.cmo ../caml/Clflags.cmo \
-    ../caml/Cil2Csyntax.cmo ../caml/Camlcoq.cmo ../caml/CMtypecheck.cmi \
-    ../caml/CMparser.cmi ../caml/CMlexer.cmi 
-../caml/Driver.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \
-    Errors.cmx Csyntax.cmx ../caml/Configuration.cmx ../caml/Clflags.cmx \
-    ../caml/Cil2Csyntax.cmx ../caml/Camlcoq.cmx ../caml/CMtypecheck.cmx \
-    ../caml/CMparser.cmx ../caml/CMlexer.cmx 
-../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo 
-../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx 
-../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTL.cmi Datatypes.cmi \
-    Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi 
-../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \
-    Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx 
-../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
-    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
-../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
-    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
-../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
-    CList.cmi AST.cmi 
-../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
-    CList.cmx AST.cmx 
-../caml/PrintPPC.cmo: PPC.cmi Datatypes.cmi ../caml/Camlcoq.cmo CList.cmi \
-    AST.cmi ../caml/PrintPPC.cmi 
-../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \
-    AST.cmx ../caml/PrintPPC.cmi 
-../caml/RTLgenaux.cmo: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \
-    ../caml/Camlcoq.cmo 
-../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \
-    ../caml/Camlcoq.cmx 
-../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \
-    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
-../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \
-    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
-Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \
-    Maps.cmi Locations.cmi LTL.cmi Errors.cmi Datatypes.cmi Coloring.cmi \
-    CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi 
-Ascii.cmi: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi 
-AST.cmi: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
-    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi 
-BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi 
-BinNat.cmi: Specif.cmi Datatypes.cmi BinPos.cmi 
-BinPos.cmi: Peano.cmi Datatypes.cmi 
-Bool.cmi: Specif.cmi Datatypes.cmi 
-Bounds.cmi: Zmax.cmi Locations.cmi Linear.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi 
-CInt.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi 
-CList.cmi: Specif.cmi Datatypes.cmi 
-Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
-    Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi \
-    Cminor.cmi CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi \
-    AST.cmi 
-Cminor.cmi: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi 
-CminorSel.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi AST.cmi 
-Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
-    Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
-    CList.cmi BinInt.cmi AST.cmi 
-Compare_dec.cmi: Specif.cmi Datatypes.cmi 
-Constprop.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
-    Floats.cmi Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Conventions.cmi: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
-    BinInt.cmi AST.cmi 
-Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi 
-CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
-    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
-Csharpminor.cmi: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \
-    AST.cmi 
-Cshmgen.cmi: Specif.cmi Peano.cmi Integers.cmi Floats.cmi Errors.cmi \
-    Datatypes.cmi Csyntax.cmi Csharpminor.cmi Cminor.cmi CString.cmi \
-    CList.cmi Ascii.cmi AST.cmi 
-CString.cmi: Specif.cmi Datatypes.cmi Ascii.cmi 
-Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \
-    Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    Ascii.cmi AST.cmi 
-Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
-    CList.cmi AST.cmi 
-EqNat.cmi: Specif.cmi Datatypes.cmi 
-Errors.cmi: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi 
-Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
-FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Datatypes.cmi \
-    CList.cmi CInt.cmi BinPos.cmi BinInt.cmi 
-FSetFacts.cmi: Specif.cmi Setoid.cmi FSetInterface.cmi Datatypes.cmi 
-FSetInterface.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
-FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
-Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \
-    CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \
-    CList.cmi Bool.cmi BinPos.cmi BinInt.cmi 
-InterfGraph.cmi: Specif.cmi Registers.cmi OrderedType.cmi Locations.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi 
-Iteration.cmi: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi 
-Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
-    Lattice.cmi Iteration.cmi Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi \
-    BinPos.cmi BinInt.cmi 
-Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
-    BinPos.cmi 
-Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
-    Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
-    CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
-Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi 
-Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
-    BinInt.cmi AST.cmi 
-LTLin.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi 
-LTL.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
-    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi 
-Mach.cmi: Values.cmi Specif.cmi Op.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi 
-Main.cmi: Tunneling.cmi Stacking.cmi Selection.cmi Reload.cmi RTLgen.cmi \
-    RTL.cmi PPCgen.cmi PPC.cmi Linearize.cmi Errors.cmi Datatypes.cmi \
-    Ctyping.cmi Csyntax.cmi Cshmgen.cmi Constprop.cmi Cminorgen.cmi \
-    Cminor.cmi CString.cmi CSE.cmi Ascii.cmi Allocation.cmi AST.cmi 
-Maps.cmi: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \
-    BinInt.cmi 
-Mem.cmi: Zmax.cmi Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \
-    CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Op.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
-    Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Ordered.cmi: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \
-    BinPos.cmi 
-OrderedType.cmi: Specif.cmi Datatypes.cmi 
-Parallelmove.cmi: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi 
-Parmov.cmi: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi 
-Peano.cmi: Datatypes.cmi 
-PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
-    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
-PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \
-    Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi 
-RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \
-    Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi Cminor.cmi \
-    CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi 
-RTL.cmi: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Errors.cmi \
-    Datatypes.cmi Coqlib.cmi Conventions.cmi CString.cmi CList.cmi Ascii.cmi \
-    AST.cmi 
-Selection.cmi: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \
-    CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Setoid.cmi: Datatypes.cmi 
-Specif.cmi: Datatypes.cmi 
-Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Linear.cmi \
-    Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
-    CString.cmi CList.cmi Bounds.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
-Sumbool.cmi: Specif.cmi Datatypes.cmi 
-Switch.cmi: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \
-    CList.cmi BinPos.cmi BinInt.cmi 
-Tunneling.cmi: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi 
-Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi 
-ZArith_dec.cmi: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi 
-Zbool.cmi: Zeven.cmi ZArith_dec.cmi Sumbool.cmi Specif.cmi Datatypes.cmi \
-    BinInt.cmi 
-Zdiv.cmi: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \
-    BinInt.cmi 
-Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi 
-Zmax.cmi: Datatypes.cmi BinInt.cmi 
-Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi 
-Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi 
-Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \
-    Maps.cmi Locations.cmi Lattice.cmi LTL.cmi Kildall.cmi Errors.cmi \
-    Datatypes.cmi Coloring.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \
-    AST.cmi Allocation.cmi 
-Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx \
-    Maps.cmx Locations.cmx Lattice.cmx LTL.cmx Kildall.cmx Errors.cmx \
-    Datatypes.cmx Coloring.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx \
-    AST.cmx Allocation.cmi 
-Ascii.cmo: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi Ascii.cmi 
-Ascii.cmx: Specif.cmx Peano.cmx Datatypes.cmx Bool.cmx BinPos.cmx Ascii.cmi 
-AST.cmo: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
-    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
-AST.cmx: Specif.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \
-    Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmi 
-BinInt.cmo: Datatypes.cmi BinPos.cmi BinNat.cmi BinInt.cmi 
-BinInt.cmx: Datatypes.cmx BinPos.cmx BinNat.cmx BinInt.cmi 
-BinNat.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinNat.cmi 
-BinNat.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinNat.cmi 
-BinPos.cmo: Peano.cmi Datatypes.cmi BinPos.cmi 
-BinPos.cmx: Peano.cmx Datatypes.cmx BinPos.cmi 
-Bool.cmo: Specif.cmi Datatypes.cmi Bool.cmi 
-Bool.cmx: Specif.cmx Datatypes.cmx Bool.cmi 
-Bounds.cmo: Zmax.cmi Locations.cmi Linear.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi Bounds.cmi 
-Bounds.cmx: Zmax.cmx Locations.cmx Linear.cmx Conventions.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx AST.cmx Bounds.cmi 
-CInt.cmo: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi CInt.cmi 
-CInt.cmx: Zmax.cmx ZArith_dec.cmx Specif.cmx BinPos.cmx BinInt.cmx CInt.cmi 
-CList.cmo: Specif.cmi Datatypes.cmi CList.cmi 
-CList.cmx: Specif.cmx Datatypes.cmx CList.cmi 
-Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
-    Maps.cmi Integers.cmi FSetAVL.cmi Errors.cmi Datatypes.cmi \
-    Csharpminor.cmi Coqlib.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi \
-    BinInt.cmi Ascii.cmi AST.cmi Cminorgen.cmi 
-Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Mem.cmx \
-    Maps.cmx Integers.cmx FSetAVL.cmx Errors.cmx Datatypes.cmx \
-    Csharpminor.cmx Coqlib.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx \
-    BinInt.cmx Ascii.cmx AST.cmx Cminorgen.cmi 
-Cminor.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi Cminor.cmi 
-Cminor.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \
-    Globalenvs.cmx Floats.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx Cminor.cmi 
-CminorSel.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi AST.cmi \
-    CminorSel.cmi 
-CminorSel.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Cminor.cmx CList.cmx BinInt.cmx AST.cmx \
-    CminorSel.cmi 
-Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
-    Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
-    ../caml/Coloringaux.cmi CList.cmi BinInt.cmi AST.cmi Coloring.cmi 
-Coloring.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx Maps.cmx \
-    Locations.cmx InterfGraph.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \
-    ../caml/Coloringaux.cmx CList.cmx BinInt.cmx AST.cmx Coloring.cmi 
-Compare_dec.cmo: Specif.cmi Datatypes.cmi Compare_dec.cmi 
-Compare_dec.cmx: Specif.cmx Datatypes.cmx Compare_dec.cmi 
-Constprop.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Lattice.cmi \
-    Kildall.cmi Integers.cmi Floats.cmi Datatypes.cmi CList.cmi Bool.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi Constprop.cmi 
-Constprop.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Lattice.cmx \
-    Kildall.cmx Integers.cmx Floats.cmx Datatypes.cmx CList.cmx Bool.cmx \
-    BinPos.cmx BinInt.cmx AST.cmx Constprop.cmi 
-Conventions.cmo: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
-    BinInt.cmi AST.cmi Conventions.cmi 
-Conventions.cmx: Locations.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \
-    BinInt.cmx AST.cmx Conventions.cmi 
-Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi Coqlib.cmi 
-Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx Datatypes.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx Coqlib.cmi 
-CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \
-    Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
-    AST.cmi CSE.cmi 
-CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \
-    Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \
-    AST.cmx CSE.cmi 
-Csharpminor.cmo: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \
-    AST.cmi Csharpminor.cmi 
-Csharpminor.cmx: Zmax.cmx Values.cmx Mem.cmx Maps.cmx Integers.cmx \
-    Globalenvs.cmx Floats.cmx Datatypes.cmx Cminor.cmx CList.cmx BinInt.cmx \
-    AST.cmx Csharpminor.cmi 
-Cshmgen.cmo: Specif.cmi Peano.cmi Integers.cmi Floats.cmi Errors.cmi \
-    Datatypes.cmi Csyntax.cmi Csharpminor.cmi Cminor.cmi CString.cmi \
-    CList.cmi Ascii.cmi AST.cmi Cshmgen.cmi 
-Cshmgen.cmx: Specif.cmx Peano.cmx Integers.cmx Floats.cmx Errors.cmx \
-    Datatypes.cmx Csyntax.cmx Csharpminor.cmx Cminor.cmx CString.cmx \
-    CList.cmx Ascii.cmx AST.cmx Cshmgen.cmi 
-CString.cmo: Specif.cmi Datatypes.cmi Ascii.cmi CString.cmi 
-CString.cmx: Specif.cmx Datatypes.cmx Ascii.cmx CString.cmi 
-Csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \
-    Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    Ascii.cmi AST.cmi Csyntax.cmi 
-Csyntax.cmx: Zmax.cmx Specif.cmx Integers.cmx Floats.cmx Errors.cmx \
-    Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    Ascii.cmx AST.cmx Csyntax.cmi 
-Ctyping.cmo: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
-    CList.cmi AST.cmi Ctyping.cmi 
-Ctyping.cmx: Specif.cmx Maps.cmx Datatypes.cmx Csyntax.cmx Coqlib.cmx \
-    CList.cmx AST.cmx Ctyping.cmi 
-Datatypes.cmo: Datatypes.cmi 
-Datatypes.cmx: Datatypes.cmi 
-EqNat.cmo: Specif.cmi Datatypes.cmi EqNat.cmi 
-EqNat.cmx: Specif.cmx Datatypes.cmx EqNat.cmi 
-Errors.cmo: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi Errors.cmi 
-Errors.cmx: Datatypes.cmx CString.cmx CList.cmx BinPos.cmx Errors.cmi 
-Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \
-    Floats.cmi 
-Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \
-    Floats.cmi 
-FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi FSetList.cmi \
-    Datatypes.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi 
-FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx FSetList.cmx \
-    Datatypes.cmx CList.cmx CInt.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi 
-FSetFacts.cmo: Specif.cmi Setoid.cmi OrderedType.cmi FSetInterface.cmi \
-    Datatypes.cmi FSetFacts.cmi 
-FSetFacts.cmx: Specif.cmx Setoid.cmx OrderedType.cmx FSetInterface.cmx \
-    Datatypes.cmx FSetFacts.cmi 
-FSetInterface.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi \
-    FSetInterface.cmi 
-FSetInterface.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx \
-    FSetInterface.cmi 
-FSetList.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi 
-FSetList.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx FSetList.cmi 
-Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \
-    CList.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi 
-Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx Integers.cmx Datatypes.cmx \
-    CList.cmx BinPos.cmx BinInt.cmx AST.cmx Globalenvs.cmi 
-Integers.cmo: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \
-    CList.cmi Bool.cmi BinPos.cmi BinInt.cmi Integers.cmi 
-Integers.cmx: Zpower.cmx Zdiv.cmx Specif.cmx Datatypes.cmx Coqlib.cmx \
-    CList.cmx Bool.cmx BinPos.cmx BinInt.cmx Integers.cmi 
-InterfGraph.cmo: Specif.cmi Registers.cmi OrderedType.cmi Ordered.cmi \
-    Locations.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
-    BinInt.cmi InterfGraph.cmi 
-InterfGraph.cmx: Specif.cmx Registers.cmx OrderedType.cmx Ordered.cmx \
-    Locations.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \
-    BinInt.cmx InterfGraph.cmi 
-Iteration.cmo: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
-    Iteration.cmi 
-Iteration.cmx: Wf.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \
-    Iteration.cmi 
-Kildall.cmo: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
-    Lattice.cmi Iteration.cmi FSetFacts.cmi FSetAVL.cmi Datatypes.cmi \
-    Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi Kildall.cmi 
-Kildall.cmx: Specif.cmx Setoid.cmx OrderedType.cmx Ordered.cmx Maps.cmx \
-    Lattice.cmx Iteration.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx \
-    Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx Kildall.cmi 
-Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
-    BinPos.cmi Lattice.cmi 
-Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \
-    BinPos.cmx Lattice.cmi 
-Linearize.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
-    ../caml/Linearizeaux.cmo Lattice.cmi LTLin.cmi LTL.cmi Kildall.cmi \
-    FSetAVL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Linearize.cmi 
-Linearize.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Maps.cmx \
-    ../caml/Linearizeaux.cmx Lattice.cmx LTLin.cmx LTL.cmx Kildall.cmx \
-    FSetAVL.cmx Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx Linearize.cmi 
-Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi Linear.cmi 
-Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx AST.cmx Linear.cmi 
-Locations.cmo: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
-    BinInt.cmi AST.cmi Locations.cmi 
-Locations.cmx: Values.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \
-    BinInt.cmx AST.cmx Locations.cmi 
-Logic.cmo: Logic.cmi 
-Logic.cmx: Logic.cmi 
-LTLin.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi LTLin.cmi 
-LTLin.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx LTLin.cmi 
-LTL.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
-    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi LTL.cmi 
-LTL.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx Locations.cmx \
-    Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx AST.cmx LTL.cmi 
-Mach.cmo: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi Mach.cmi 
-Mach.cmx: Values.cmx Specif.cmx Op.cmx Maps.cmx Locations.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx Mach.cmi 
-Main.cmo: Tunneling.cmi Stacking.cmi Selection.cmi Reload.cmi RTLgen.cmi \
-    RTL.cmi PPCgen.cmi PPC.cmi Linearize.cmi Errors.cmi Datatypes.cmi \
-    Ctyping.cmi Csyntax.cmi Cshmgen.cmi Constprop.cmi Cminorgen.cmi \
-    Cminor.cmi CString.cmi CSE.cmi Ascii.cmi Allocation.cmi AST.cmi Main.cmi 
-Main.cmx: Tunneling.cmx Stacking.cmx Selection.cmx Reload.cmx RTLgen.cmx \
-    RTL.cmx PPCgen.cmx PPC.cmx Linearize.cmx Errors.cmx Datatypes.cmx \
-    Ctyping.cmx Csyntax.cmx Cshmgen.cmx Constprop.cmx Cminorgen.cmx \
-    Cminor.cmx CString.cmx CSE.cmx Ascii.cmx Allocation.cmx AST.cmx Main.cmi 
-Maps.cmo: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \
-    BinInt.cmi Maps.cmi 
-Maps.cmx: Specif.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinNat.cmx \
-    BinInt.cmx Maps.cmi 
-Mem.cmo: Zmax.cmi Values.cmi Specif.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \
-    CList.cmi BinPos.cmi BinInt.cmi AST.cmi Mem.cmi 
-Mem.cmx: Zmax.cmx Values.cmx Specif.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \
-    CList.cmx BinPos.cmx BinInt.cmx AST.cmx Mem.cmi 
-Op.cmo: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
-    Datatypes.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Op.cmi 
-Op.cmx: Values.cmx Specif.cmx Mem.cmx Integers.cmx Globalenvs.cmx Floats.cmx \
-    Datatypes.cmx CList.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Op.cmi 
-Ordered.cmo: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \
-    BinPos.cmi Ordered.cmi 
-Ordered.cmx: Specif.cmx OrderedType.cmx Maps.cmx Datatypes.cmx Coqlib.cmx \
-    BinPos.cmx Ordered.cmi 
-OrderedType.cmo: Specif.cmi Datatypes.cmi OrderedType.cmi 
-OrderedType.cmx: Specif.cmx Datatypes.cmx OrderedType.cmi 
-Parallelmove.cmo: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi \
-    Parallelmove.cmi 
-Parallelmove.cmx: Parmov.cmx Locations.cmx Datatypes.cmx CList.cmx AST.cmx \
-    Parallelmove.cmi 
-Parmov.cmo: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Parmov.cmi 
-Parmov.cmx: Specif.cmx Peano.cmx Datatypes.cmx CList.cmx Parmov.cmi 
-Peano.cmo: Datatypes.cmi Peano.cmi 
-Peano.cmx: Datatypes.cmx Peano.cmi 
-PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
-    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi PPCgen.cmi 
-PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \
-    Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx Bool.cmx \
-    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx PPCgen.cmi 
-PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \
-    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi PPC.cmi 
-PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \
-    Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx PPC.cmi 
-Registers.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi FSetAVL.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
-    Registers.cmi 
-Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \
-    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
-    Registers.cmi 
-Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi \
-    Reload.cmi 
-Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \
-    LTLin.cmx Integers.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx \
-    Reload.cmi 
-RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \
-    Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
-    CminorSel.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \
-    AST.cmi RTLgen.cmi 
-RTLgen.cmx: Switch.cmx Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx \
-    Op.cmx Maps.cmx Integers.cmx Errors.cmx Datatypes.cmx Coqlib.cmx \
-    CminorSel.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx \
-    AST.cmx RTLgen.cmi 
-RTL.cmo: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
-    RTL.cmi 
-RTL.cmx: Values.cmx Registers.cmx Op.cmx Mem.cmx Maps.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
-    RTL.cmi 
-RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \
-    Op.cmi Maps.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
-    CString.cmi CList.cmi Ascii.cmi AST.cmi RTLtyping.cmi 
-RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \
-    Op.cmx Maps.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \
-    CString.cmx CList.cmx Ascii.cmx AST.cmx RTLtyping.cmi 
-Selection.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \
-    CminorSel.cmi Cminor.cmi ../caml/Clflags.cmo CList.cmi BinPos.cmi \
-    BinInt.cmi AST.cmi Selection.cmi 
-Selection.cmx: Specif.cmx Op.cmx Integers.cmx Datatypes.cmx Compare_dec.cmx \
-    CminorSel.cmx Cminor.cmx ../caml/Clflags.cmx CList.cmx BinPos.cmx \
-    BinInt.cmx AST.cmx Selection.cmi 
-Setoid.cmo: Datatypes.cmi Setoid.cmi 
-Setoid.cmx: Datatypes.cmx Setoid.cmi 
-Specif.cmo: Datatypes.cmi Specif.cmi 
-Specif.cmx: Datatypes.cmx Specif.cmi 
-Stacking.cmo: Specif.cmi Op.cmi Mach.cmi Locations.cmi Linear.cmi \
-    Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
-    CString.cmi CList.cmi Bounds.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi \
-    Stacking.cmi 
-Stacking.cmx: Specif.cmx Op.cmx Mach.cmx Locations.cmx Linear.cmx \
-    Integers.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \
-    CString.cmx CList.cmx Bounds.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx \
-    Stacking.cmi 
-Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi 
-Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi 
-Switch.cmo: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \
-    CList.cmi BinPos.cmi BinInt.cmi Switch.cmi 
-Switch.cmx: Specif.cmx Integers.cmx EqNat.cmx Datatypes.cmx Coqlib.cmx \
-    CList.cmx BinPos.cmx BinInt.cmx Switch.cmi 
-Tunneling.cmo: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi 
-Tunneling.cmx: Maps.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi 
-Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi Values.cmi 
-Values.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \
-    BinPos.cmx BinInt.cmx AST.cmx Values.cmi 
-Wf.cmo: Wf.cmi 
-Wf.cmx: Wf.cmi 
-ZArith_dec.cmo: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi \
-    ZArith_dec.cmi 
-ZArith_dec.cmx: Sumbool.cmx Specif.cmx Datatypes.cmx BinInt.cmx \
-    ZArith_dec.cmi 
-Zbool.cmo: Zeven.cmi ZArith_dec.cmi Sumbool.cmi Specif.cmi Datatypes.cmi \
-    BinInt.cmi Zbool.cmi 
-Zbool.cmx: Zeven.cmx ZArith_dec.cmx Sumbool.cmx Specif.cmx Datatypes.cmx \
-    BinInt.cmx Zbool.cmi 
-Zdiv.cmo: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \
-    BinInt.cmi Zdiv.cmi 
-Zdiv.cmx: Zbool.cmx ZArith_dec.cmx Specif.cmx Datatypes.cmx BinPos.cmx \
-    BinInt.cmx Zdiv.cmi 
-Zeven.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zeven.cmi 
-Zeven.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zeven.cmi 
-Zmax.cmo: Datatypes.cmi BinInt.cmi Zmax.cmi 
-Zmax.cmx: Datatypes.cmx BinInt.cmx Zmax.cmi 
-Zmisc.cmo: Datatypes.cmi BinPos.cmi BinInt.cmi Zmisc.cmi 
-Zmisc.cmx: Datatypes.cmx BinPos.cmx BinInt.cmx Zmisc.cmi 
-Zpower.cmo: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi 
-Zpower.cmx: Zmisc.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zpower.cmi 
diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch
index a5b7bc9..453d40c 100644
--- a/extraction/Kildall.ml.patch
+++ b/extraction/Kildall.ml.patch
@@ -1,5 +1,5 @@
-*** Kildall.ml.orig	2006-09-11 13:50:56.266682206 +0200
---- Kildall.ml	2006-09-11 14:29:50.392200227 +0200
+*** kildall.ml.orig	2006-09-11 13:50:56.266682206 +0200
+--- kildall.ml	2006-09-11 14:29:50.392200227 +0200
 ***************
 *** 163,171 ****
                        Maps.PMap.t option **)
diff --git a/extraction/Makefile b/extraction/Makefile
index 044f89f..d4163bb 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -12,66 +12,15 @@
 
 include ../Makefile.config
 
-FILES=\
-  Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml EqNat.ml \
-  Bool.ml CList.ml Sumbool.ml Setoid.ml BinPos.ml BinNat.ml BinInt.ml \
-  ZArith_dec.ml Zeven.ml Zmax.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \
-  Ascii.ml CString.ml \
-  OrderedType.ml FSetInterface.ml FSetFacts.ml FSetList.ml \
-  CInt.ml FSetAVL.ml \
-  Coqlib.ml Maps.ml Ordered.ml Errors.ml AST.ml Iteration.ml Integers.ml \
-  ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \
-  Mem.ml Globalenvs.ml \
-  ../caml/Clflags.ml \
-  Csyntax.ml Ctyping.ml Cminor.ml Csharpminor.ml Cshmgen.ml \
-  Cminorgen.ml \
-  Op.ml CminorSel.ml \
-  Selection.ml \
-  Registers.ml RTL.ml \
-  Switch.ml ../caml/RTLgenaux.ml RTLgen.ml \
-  Locations.ml Conventions.ml \
-  ../caml/RTLtypingaux.ml RTLtyping.ml \
-  Lattice.ml Kildall.ml \
-  Constprop.ml CSE.ml \
-  LTL.ml LTLin.ml \
-  InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \
-  Allocation.ml  \
-  Tunneling.ml Linear.ml ../caml/Linearizeaux.ml Linearize.ml \
-  Parallelmove.ml Reload.ml \
-  Mach.ml Bounds.ml Stacking.ml \
-  PPC.ml PPCgen.ml \
-  Main.ml \
-  ../caml/PrintCsyntax.ml ../caml/Cil2Csyntax.ml \
-  ../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \
-  ../caml/PrintPPC.ml \
-  ../caml/Configuration.ml ../caml/Driver.ml
+DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver
 
-EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES))
-GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli)
-
-CAMLINCL=-I ../caml -I ../cil/obj/$(ARCHOS)
-OCAMLC=ocamlc -g $(CAMLINCL)
-OCAMLOPT=ocamlopt $(CAMLINCL)
-OCAMLDEP=ocamldep $(CAMLINCL)
-OCAMLLIBS=unix.cma str.cma cil.cma
-
-COQINCL=-I ../lib -I ../common -I ../backend -I ../cfrontend
+COQINCL=$(patsubst %,-I ../%,$(DIRS))
 COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source
 
-executables: ../ccomp ../ccomp.byt
-
-../ccomp.byt: $(FILES:.ml=.cmo)
-	$(OCAMLC) -o ../ccomp.byt $(OCAMLLIBS) $(FILES:.ml=.cmo)
-clean::
-	rm -f ../ccomp.byt
-
-../ccomp: $(FILES:.ml=.cmx)
-	$(OCAMLOPT) -o ../ccomp $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx)
-clean::
-	rm -f ../ccomp
+all: Configuration.ml extraction
 
 extraction:
-	@rm -f $(GENFILES)
+	rm -f [:lower:]*.mli [:lower:]*.ml
 	$(COQEXEC) extraction.v
 	@echo "Fixing file names..."
 	@mv list.ml CList.ml
@@ -80,61 +29,19 @@ extraction:
 	@mv string.mli CString.mli
 	@mv int.ml CInt.ml
 	@mv int.mli CInt.mli
-	@for i in $(GENFILES); do \
-          j=`./uncapitalize $$i`; \
-          test -f $$i || (test -f $$j && mv $$j $$i); \
-         done
 	@echo "Conversion List -> CList, String -> CString, Int -> CInt..."
-	@./convert $(GENFILES)
+	@./convert *.mli *.ml
 	@echo "Patching files..."
 	@for i in *.patch; do patch < $$i; done
 
-../caml/CMparser.ml ../caml/CMparser.mli: ../caml/CMparser.mly
-	ocamlyacc -v ../caml/CMparser.mly
-
-beforedepend:: ../caml/CMparser.ml ../caml/CMparser.mli
-clean::
-	rm -f ../caml/CMparser.ml ../caml/CMparser.mli ../caml/CMparser.output
-
-../caml/CMlexer.ml: ../caml/CMlexer.mll
-	ocamllex ../caml/CMlexer.mll
-
-beforedepend:: ../caml/CMlexer.ml
-clean::
-	rm -f ../caml/CMlexer.ml
-
-../caml/Configuration.ml: ../Makefile.config
+Configuration.ml: ../Makefile.config
 	(echo 'let stdlib_path = "$(LIBDIR)"'; \
          echo 'let prepro = "$(CPREPRO)"'; \
          echo 'let asm = "$(CASM)"'; \
-         echo 'let linker = "$(CLINKER)"') \
-        > ../caml/Configuration.ml
-
-beforedepend:: ../caml/Configuration.ml
-clean::
-	rm -f ../caml/Configuration.ml
-
-.SUFFIXES: .ml .mli .cmo .cmi .cmx
-
-.mli.cmi:
-	$(OCAMLC) -c $*.mli
-.ml.cmo:
-	$(OCAMLC) -c $*.ml
-.ml.cmx:
-	$(OCAMLOPT) -c $*.ml
-
-clean::
-	rm -f $(GENFILES)
-	rm -f *.cm? *.o
-	cd ../caml && rm -f *.cm? *.o
-
-depend: beforedepend
-	$(OCAMLDEP) ../caml/*.mli ../caml/*.ml *.mli *.ml > .depend
-
-install:
-	install -d $(BINDIR)
-	install ../ccomp ../ccomp.byt $(BINDIR)
-
-include .depend
-
+         echo 'let linker = "$(CLINKER)"'; \
+         echo 'let arch = "$(ARCH)"'; \
+         echo 'let variant = "$(VARIANT)"') \
+        > Configuration.ml
 
+clean:
+	rm -f *.mli *.ml
diff --git a/extraction/extraction.v b/extraction/extraction.v
index cdb1fd6..58da9c0 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -16,7 +16,7 @@ Require Floats.
 Require RTLgen.
 Require Coloring.
 Require Allocation.
-Require Main.
+Require Compiler.
 
 (* Standard lib *)
 Extract Inductive unit => "unit" [ "()" ].
@@ -68,16 +68,18 @@ Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
 (* Linearize *)
 Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 
-(* PPC *)
-Extract Constant PPC.low_half => "fun _ -> assert false".
-Extract Constant PPC.high_half => "fun _ -> assert false".
+(* Asm *)
+Extract Constant Asm.low_half => "fun _ -> assert false".
+Extract Constant Asm.high_half => "fun _ -> assert false".
 
 (* Suppression of stupidly big equality functions *)
-Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y".
-Extract Constant Locations.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y".
-Extract Constant PPC.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
-Extract Constant PPC.freg_eq => "fun (x: freg) (y: freg) -> x = y".
-Extract Constant PPC.preg_eq => "fun (x: preg) (y: preg) -> x = y".
+Extract Constant Op.eq_operation => "fun (x: operation) (y: operation) -> x = y".
+Extract Constant Op.eq_addressing => "fun (x: addressing) (y: addressing) -> x = y".
+(*Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y".*)
+Extract Constant Machregs.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y".
+Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
+Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
+Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
 
 (* Go! *)
-Recursive Extraction Library Main.
+Recursive Extraction Library Compiler.