Initial import of compcert

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

6 files changed, 589 insertions, 0 deletions

diff --git a/extraction/.depend b/extraction/.depend
new file mode 100644
index 0000000..1067a0a
--- /dev/null
+++ b/extraction/.depend
@@ -0,0 +1,395 @@
+../caml/Allocationaux.cmi: Locations.cmi List.cmi Datatypes.cmi 
+../caml/CMlexer.cmi: ../caml/CMparser.cmi 
+../caml/CMparser.cmi: Cminor.cmi AST.cmi 
+../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \
+    InterfGraph.cmi 
+../caml/PrintPPC.cmi: PPC.cmi 
+../caml/Allocationaux.cmo: Locations.cmi List.cmi Datatypes.cmi \
+    ../caml/Camlcoq.cmo AST.cmi ../caml/Allocationaux.cmi 
+../caml/Allocationaux.cmx: Locations.cmx List.cmx Datatypes.cmx \
+    ../caml/Camlcoq.cmx AST.cmx ../caml/Allocationaux.cmi 
+../caml/Camlcoq.cmo: List.cmi Integers.cmi Datatypes.cmi BinPos.cmi \
+    BinInt.cmi 
+../caml/Camlcoq.cmx: List.cmx Integers.cmx Datatypes.cmx BinPos.cmx \
+    BinInt.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: Op.cmi List.cmi Integers.cmi Datatypes.cmi Cminor.cmi \
+    Cmconstr.cmi ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi \
+    ../caml/CMparser.cmi 
+../caml/CMparser.cmx: Op.cmx List.cmx Integers.cmx Datatypes.cmx Cminor.cmx \
+    Cmconstr.cmx ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx \
+    ../caml/CMparser.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/Floataux.cmo: ../caml/Camlcoq.cmo AST.cmi 
+../caml/Floataux.cmx: ../caml/Camlcoq.cmx AST.cmx 
+../caml/Main2.cmo: ../caml/PrintPPC.cmi Main.cmi Datatypes.cmi \
+    ../caml/CMparser.cmi ../caml/CMlexer.cmi 
+../caml/Main2.cmx: ../caml/PrintPPC.cmx Main.cmx Datatypes.cmx \
+    ../caml/CMparser.cmx ../caml/CMlexer.cmx 
+../caml/PrintPPC.cmo: PPC.cmi List.cmi Datatypes.cmi ../caml/Camlcoq.cmo \
+    AST.cmi ../caml/PrintPPC.cmi 
+../caml/PrintPPC.cmx: PPC.cmx List.cmx Datatypes.cmx ../caml/Camlcoq.cmx \
+    AST.cmx ../caml/PrintPPC.cmi 
+../caml/RTLgenaux.cmo: Cminor.cmi 
+../caml/RTLgenaux.cmx: Cminor.cmx 
+Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \
+    Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi List.cmi LTL.cmi \
+    Datatypes.cmi Conventions.cmi Coloring.cmi BinPos.cmi AST.cmi 
+AST.cmi: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi 
+BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi 
+BinNat.cmi: Datatypes.cmi BinPos.cmi 
+BinPos.cmi: Peano.cmi Datatypes.cmi 
+Bool.cmi: Specif.cmi Datatypes.cmi 
+Cmconstr.cmi: Specif.cmi Op.cmi List.cmi Integers.cmi Datatypes.cmi \
+    Compare_dec.cmi Cminor.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Cminorgen.cmi: Zmin.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi List.cmi \
+    Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \
+    Cmconstr.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Cminor.cmi: Values.cmi Op.cmi Maps.cmi List.cmi Globalenvs.cmi Datatypes.cmi \
+    BinInt.cmi AST.cmi 
+Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
+    Locations.cmi List.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi \
+    Conventions.cmi BinInt.cmi AST.cmi 
+Compare_dec.cmi: Specif.cmi Datatypes.cmi 
+Constprop.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \
+    Integers.cmi Floats.cmi Datatypes.cmi Bool.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi 
+Conventions.cmi: Locations.cmi List.cmi Datatypes.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi 
+Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi List.cmi Datatypes.cmi \
+    BinPos.cmi BinInt.cmi 
+CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \
+    Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi 
+Csharpminor.cmi: Zmin.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi List.cmi \
+    Integers.cmi Globalenvs.cmi Floats.cmi Datatypes.cmi BinPos.cmi \
+    BinInt.cmi AST.cmi 
+Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi AST.cmi 
+FSetAVL.cmi: ZArith_dec.cmi Wf.cmi Specif.cmi Peano.cmi List.cmi \
+    FSetInterface.cmi Datatypes.cmi BinPos.cmi BinInt.cmi 
+FSetBridge.cmi: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi 
+FSetInterface.cmi: Specif.cmi List.cmi Datatypes.cmi 
+FSetList.cmi: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi 
+Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi List.cmi Integers.cmi \
+    Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi List.cmi Datatypes.cmi \
+    Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi 
+InterfGraph.cmi: Specif.cmi Registers.cmi Locations.cmi List.cmi \
+    FSetInterface.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi 
+Kildall.cmi: Wf.cmi Specif.cmi Maps.cmi List.cmi Lattice.cmi Datatypes.cmi \
+    Coqlib.cmi BinPos.cmi 
+Lattice.cmi: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi 
+Linearize.cmi: Specif.cmi Op.cmi Maps.cmi List.cmi Linear.cmi Lattice.cmi \
+    LTL.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi 
+Linear.cmi: Values.cmi Specif.cmi Op.cmi Locations.cmi List.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Lineartyping.cmi: Zmin.cmi Locations.cmi List.cmi Linear.cmi Datatypes.cmi \
+    Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi 
+List.cmi: Specif.cmi Datatypes.cmi 
+Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
+    BinInt.cmi AST.cmi 
+LTL.cmi: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi List.cmi \
+    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi BinPos.cmi \
+    BinInt.cmi AST.cmi 
+Mach.cmi: Zmin.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi \
+    Locations.cmi List.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \
+    Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Main.cmi: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \
+    Linearize.cmi Datatypes.cmi Csharpminor.cmi Constprop.cmi Cminorgen.cmi \
+    Cminor.cmi CSE.cmi Allocation.cmi AST.cmi 
+Maps.cmi: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinNat.cmi \
+    BinInt.cmi 
+Mem.cmi: Values.cmi Specif.cmi List.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \
+    BinPos.cmi BinInt.cmi AST.cmi 
+Op.cmi: Values.cmi Specif.cmi List.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
+    Datatypes.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Ordered.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Coqlib.cmi \
+    BinPos.cmi 
+Parallelmove.cmi: Wf.cmi Values.cmi Specif.cmi Peano.cmi Locations.cmi \
+    List.cmi LTL.cmi Datatypes.cmi AST.cmi 
+Peano.cmi: Datatypes.cmi 
+PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi List.cmi \
+    Integers.cmi Datatypes.cmi Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi 
+PPC.cmi: Values.cmi Specif.cmi Mem.cmi List.cmi Integers.cmi Globalenvs.cmi \
+    Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Registers.cmi: Specif.cmi Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi \
+    BinPos.cmi AST.cmi 
+RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \
+    Datatypes.cmi Coqlib.cmi Cminor.cmi BinPos.cmi AST.cmi 
+RTL.cmi: Values.cmi Registers.cmi Op.cmi Maps.cmi List.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi 
+RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \
+    Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi 
+Sets.cmi: Specif.cmi Maps.cmi List.cmi Datatypes.cmi 
+Specif.cmi: Datatypes.cmi 
+Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi List.cmi \
+    Lineartyping.cmi Linear.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \
+    Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Sumbool.cmi: Specif.cmi Datatypes.cmi 
+Tunneling.cmi: Maps.cmi List.cmi LTL.cmi Datatypes.cmi AST.cmi 
+union_find.cmi: Wf.cmi Specif.cmi Datatypes.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 
+Zmin.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 \
+    Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi List.cmi LTL.cmi \
+    Kildall.cmi Datatypes.cmi Conventions.cmi Coloring.cmi BinPos.cmi AST.cmi \
+    Allocation.cmi 
+Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx \
+    Parallelmove.cmx Op.cmx Maps.cmx Locations.cmx List.cmx LTL.cmx \
+    Kildall.cmx Datatypes.cmx Conventions.cmx Coloring.cmx BinPos.cmx AST.cmx \
+    Allocation.cmi 
+AST.cmo: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi 
+AST.cmx: Specif.cmx List.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinInt.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: Datatypes.cmi BinPos.cmi BinNat.cmi 
+BinNat.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 
+Cmconstr.cmo: Specif.cmi Op.cmi List.cmi Integers.cmi Datatypes.cmi \
+    Compare_dec.cmi Cminor.cmi BinPos.cmi BinInt.cmi AST.cmi Cmconstr.cmi 
+Cmconstr.cmx: Specif.cmx Op.cmx List.cmx Integers.cmx Datatypes.cmx \
+    Compare_dec.cmx Cminor.cmx BinPos.cmx BinInt.cmx AST.cmx Cmconstr.cmi 
+Cminorgen.cmo: Zmin.cmi Specif.cmi Sets.cmi Op.cmi Mem.cmi Maps.cmi List.cmi \
+    Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \
+    Cmconstr.cmi BinPos.cmi BinInt.cmi AST.cmi Cminorgen.cmi 
+Cminorgen.cmx: Zmin.cmx Specif.cmx Sets.cmx Op.cmx Mem.cmx Maps.cmx List.cmx \
+    Integers.cmx Datatypes.cmx Csharpminor.cmx Coqlib.cmx Cminor.cmx \
+    Cmconstr.cmx BinPos.cmx BinInt.cmx AST.cmx Cminorgen.cmi 
+Cminor.cmo: Values.cmi Op.cmi Maps.cmi List.cmi Globalenvs.cmi Datatypes.cmi \
+    BinInt.cmi AST.cmi Cminor.cmi 
+Cminor.cmx: Values.cmx Op.cmx Maps.cmx List.cmx Globalenvs.cmx Datatypes.cmx \
+    BinInt.cmx AST.cmx Cminor.cmi 
+Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
+    Locations.cmi List.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi \
+    Conventions.cmi ../caml/Coloringaux.cmi BinInt.cmi AST.cmi Coloring.cmi 
+Coloring.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx Maps.cmx \
+    Locations.cmx List.cmx InterfGraph.cmx Datatypes.cmx Coqlib.cmx \
+    Conventions.cmx ../caml/Coloringaux.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 List.cmi \
+    Lattice.cmi Kildall.cmi Integers.cmi Floats.cmi Datatypes.cmi Bool.cmi \
+    BinPos.cmi BinInt.cmi AST.cmi Constprop.cmi 
+Constprop.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx List.cmx \
+    Lattice.cmx Kildall.cmx Integers.cmx Floats.cmx Datatypes.cmx Bool.cmx \
+    BinPos.cmx BinInt.cmx AST.cmx Constprop.cmi 
+Conventions.cmo: Locations.cmi List.cmi Datatypes.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi Conventions.cmi 
+Conventions.cmx: Locations.cmx List.cmx Datatypes.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx Conventions.cmi 
+Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi List.cmi Datatypes.cmi \
+    BinPos.cmi BinInt.cmi Coqlib.cmi 
+Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx List.cmx Datatypes.cmx \
+    BinPos.cmx BinInt.cmx Coqlib.cmi 
+CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi List.cmi \
+    Kildall.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
+    AST.cmi CSE.cmi 
+CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx List.cmx \
+    Kildall.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \
+    AST.cmx CSE.cmi 
+Csharpminor.cmo: Zmin.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi List.cmi \
+    Integers.cmi Globalenvs.cmi Floats.cmi Datatypes.cmi BinPos.cmi \
+    BinInt.cmi AST.cmi Csharpminor.cmi 
+Csharpminor.cmx: Zmin.cmx Values.cmx Specif.cmx Mem.cmx Maps.cmx List.cmx \
+    Integers.cmx Globalenvs.cmx Floats.cmx Datatypes.cmx BinPos.cmx \
+    BinInt.cmx AST.cmx Csharpminor.cmi 
+Datatypes.cmo: Datatypes.cmi 
+Datatypes.cmx: Datatypes.cmi 
+Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \
+    AST.cmi Floats.cmi 
+Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \
+    AST.cmx Floats.cmi 
+FSetAVL.cmo: ZArith_dec.cmi Wf.cmi Specif.cmi Peano.cmi List.cmi FSetList.cmi \
+    FSetInterface.cmi Datatypes.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi 
+FSetAVL.cmx: ZArith_dec.cmx Wf.cmx Specif.cmx Peano.cmx List.cmx FSetList.cmx \
+    FSetInterface.cmx Datatypes.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi 
+FSetBridge.cmo: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi \
+    FSetBridge.cmi 
+FSetBridge.cmx: Specif.cmx List.cmx FSetInterface.cmx Datatypes.cmx \
+    FSetBridge.cmi 
+FSetInterface.cmo: Specif.cmi List.cmi Datatypes.cmi FSetInterface.cmi 
+FSetInterface.cmx: Specif.cmx List.cmx Datatypes.cmx FSetInterface.cmi 
+FSetList.cmo: Specif.cmi List.cmi FSetInterface.cmi Datatypes.cmi \
+    FSetList.cmi 
+FSetList.cmx: Specif.cmx List.cmx FSetInterface.cmx Datatypes.cmx \
+    FSetList.cmi 
+Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi List.cmi Integers.cmi \
+    Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi 
+Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx List.cmx Integers.cmx \
+    Datatypes.cmx BinPos.cmx BinInt.cmx AST.cmx Globalenvs.cmi 
+Integers.cmo: Zpower.cmi Zdiv.cmi Specif.cmi List.cmi Datatypes.cmi \
+    Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Integers.cmi 
+Integers.cmx: Zpower.cmx Zdiv.cmx Specif.cmx List.cmx Datatypes.cmx \
+    Coqlib.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Integers.cmi 
+InterfGraph.cmo: Specif.cmi Registers.cmi Ordered.cmi Locations.cmi List.cmi \
+    FSetInterface.cmi FSetBridge.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi \
+    BinPos.cmi BinInt.cmi InterfGraph.cmi 
+InterfGraph.cmx: Specif.cmx Registers.cmx Ordered.cmx Locations.cmx List.cmx \
+    FSetInterface.cmx FSetBridge.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx \
+    BinPos.cmx BinInt.cmx InterfGraph.cmi 
+Kildall.cmo: Wf.cmi Specif.cmi Maps.cmi List.cmi Lattice.cmi Datatypes.cmi \
+    Coqlib.cmi BinPos.cmi Kildall.cmi 
+Kildall.cmx: Wf.cmx Specif.cmx Maps.cmx List.cmx Lattice.cmx Datatypes.cmx \
+    Coqlib.cmx BinPos.cmx Kildall.cmi 
+Lattice.cmo: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi Lattice.cmi 
+Lattice.cmx: Specif.cmx Maps.cmx Datatypes.cmx BinPos.cmx Lattice.cmi 
+Linearize.cmo: Specif.cmi Op.cmi Maps.cmi List.cmi Linear.cmi Lattice.cmi \
+    LTL.cmi Kildall.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi \
+    Linearize.cmi 
+Linearize.cmx: Specif.cmx Op.cmx Maps.cmx List.cmx Linear.cmx Lattice.cmx \
+    LTL.cmx Kildall.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx AST.cmx \
+    Linearize.cmi 
+Linear.cmo: Values.cmi Specif.cmi Op.cmi Locations.cmi List.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi \
+    Linear.cmi 
+Linear.cmx: Values.cmx Specif.cmx Op.cmx Locations.cmx List.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinInt.cmx AST.cmx \
+    Linear.cmi 
+Lineartyping.cmo: Zmin.cmi Locations.cmi List.cmi Linear.cmi Datatypes.cmi \
+    Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi Lineartyping.cmi 
+Lineartyping.cmx: Zmin.cmx Locations.cmx List.cmx Linear.cmx Datatypes.cmx \
+    Conventions.cmx BinPos.cmx BinInt.cmx AST.cmx Lineartyping.cmi 
+List.cmo: Specif.cmi Datatypes.cmi List.cmi 
+List.cmx: Specif.cmx Datatypes.cmx List.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 
+LTL.cmo: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi List.cmi \
+    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi BinPos.cmi \
+    BinInt.cmi AST.cmi LTL.cmi 
+LTL.cmx: Values.cmx Specif.cmx Op.cmx Maps.cmx Locations.cmx List.cmx \
+    Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx BinPos.cmx \
+    BinInt.cmx AST.cmx LTL.cmi 
+Mach.cmo: Zmin.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi \
+    Locations.cmi List.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \
+    Coqlib.cmi BinPos.cmi BinInt.cmi AST.cmi Mach.cmi 
+Mach.cmx: Zmin.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx \
+    Locations.cmx List.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx \
+    Coqlib.cmx BinPos.cmx BinInt.cmx AST.cmx Mach.cmi 
+Main.cmo: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \
+    Linearize.cmi Datatypes.cmi Csharpminor.cmi Constprop.cmi Cminorgen.cmi \
+    Cminor.cmi CSE.cmi Allocation.cmi AST.cmi Main.cmi 
+Main.cmx: Tunneling.cmx Stacking.cmx RTLgen.cmx PPCgen.cmx PPC.cmx \
+    Linearize.cmx Datatypes.cmx Csharpminor.cmx Constprop.cmx Cminorgen.cmx \
+    Cminor.cmx CSE.cmx Allocation.cmx AST.cmx Main.cmi 
+Maps.cmo: Specif.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinNat.cmi \
+    BinInt.cmi Maps.cmi 
+Maps.cmx: Specif.cmx List.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinNat.cmx \
+    BinInt.cmx Maps.cmi 
+Mem.cmo: Values.cmi Specif.cmi List.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \
+    BinPos.cmi BinInt.cmi AST.cmi Mem.cmi 
+Mem.cmx: Values.cmx Specif.cmx List.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \
+    BinPos.cmx BinInt.cmx AST.cmx Mem.cmi 
+Op.cmo: Values.cmi Specif.cmi List.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
+    Datatypes.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Op.cmi 
+Op.cmx: Values.cmx Specif.cmx List.cmx Integers.cmx Globalenvs.cmx Floats.cmx \
+    Datatypes.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx Op.cmi 
+Ordered.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Coqlib.cmi \
+    BinPos.cmi Ordered.cmi 
+Ordered.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Coqlib.cmx \
+    BinPos.cmx Ordered.cmi 
+Parallelmove.cmo: Wf.cmi Values.cmi Specif.cmi Peano.cmi Locations.cmi \
+    List.cmi LTL.cmi Datatypes.cmi AST.cmi Parallelmove.cmi 
+Parallelmove.cmx: Wf.cmx Values.cmx Specif.cmx Peano.cmx Locations.cmx \
+    List.cmx LTL.cmx Datatypes.cmx AST.cmx Parallelmove.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 List.cmi \
+    Integers.cmi Datatypes.cmi Coqlib.cmi Bool.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi PPCgen.cmi 
+PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx List.cmx \
+    Integers.cmx Datatypes.cmx Coqlib.cmx Bool.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx PPCgen.cmi 
+PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi List.cmi Integers.cmi \
+    Globalenvs.cmi Floats.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi PPC.cmi 
+PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx List.cmx Integers.cmx \
+    Globalenvs.cmx Floats.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx PPC.cmi 
+Registers.cmo: Specif.cmi Sets.cmi Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi \
+    BinPos.cmi AST.cmi Registers.cmi 
+Registers.cmx: Specif.cmx Sets.cmx Maps.cmx List.cmx Datatypes.cmx Coqlib.cmx \
+    BinPos.cmx AST.cmx Registers.cmi 
+RTLgen.cmo: Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi Op.cmi \
+    Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi Cminor.cmi BinPos.cmi AST.cmi \
+    RTLgen.cmi 
+RTLgen.cmx: Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx Op.cmx \
+    Maps.cmx List.cmx Datatypes.cmx Coqlib.cmx Cminor.cmx BinPos.cmx AST.cmx \
+    RTLgen.cmi 
+RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi List.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi BinPos.cmi BinInt.cmi AST.cmi RTL.cmi 
+RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx List.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi 
+RTLtyping.cmo: union_find.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi \
+    Maps.cmi List.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi AST.cmi \
+    RTLtyping.cmi 
+RTLtyping.cmx: union_find.cmx Specif.cmx Registers.cmx RTL.cmx Op.cmx \
+    Maps.cmx List.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx AST.cmx \
+    RTLtyping.cmi 
+Sets.cmo: Specif.cmi Maps.cmi List.cmi Datatypes.cmi Sets.cmi 
+Sets.cmx: Specif.cmx Maps.cmx List.cmx Datatypes.cmx Sets.cmi 
+Specif.cmo: Datatypes.cmi Specif.cmi 
+Specif.cmx: Datatypes.cmx Specif.cmi 
+Stacking.cmo: Specif.cmi Op.cmi Mach.cmi Locations.cmi List.cmi \
+    Lineartyping.cmi Linear.cmi Integers.cmi Datatypes.cmi Coqlib.cmi \
+    Conventions.cmi BinPos.cmi BinInt.cmi AST.cmi Stacking.cmi 
+Stacking.cmx: Specif.cmx Op.cmx Mach.cmx Locations.cmx List.cmx \
+    Lineartyping.cmx Linear.cmx Integers.cmx Datatypes.cmx Coqlib.cmx \
+    Conventions.cmx BinPos.cmx BinInt.cmx AST.cmx Stacking.cmi 
+Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi 
+Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi 
+Tunneling.cmo: Maps.cmi List.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi 
+Tunneling.cmx: Maps.cmx List.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi 
+union_find.cmo: Wf.cmi Specif.cmi Datatypes.cmi union_find.cmi 
+union_find.cmx: Wf.cmx Specif.cmx Datatypes.cmx union_find.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 
+Zmin.cmo: Datatypes.cmi BinInt.cmi Zmin.cmi 
+Zmin.cmx: Datatypes.cmx BinInt.cmx Zmin.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
new file mode 100644
index 0000000..a091385
--- /dev/null
+++ b/extraction/Kildall.ml.patch
@@ -0,0 +1,22 @@
+*** Kildall.ml.orig	2006-02-09 11:47:52.000000000 +0100
+--- Kildall.ml	2006-02-09 13:42:35.103321691 +0100
+***************
+*** 191,199 ****
+                       Maps.PMap.t option **)
+    
+    let fixpoint successors topnode transf entrypoints =
+!     DS.fixpoint (fun s ->
+!       Maps.PMap.get s (make_predecessors successors topnode)) topnode transf
+!       entrypoints
+   end
+  
+  module type ORDERED_TYPE_WITH_TOP = 
+--- 191,198 ----
+                       Maps.PMap.t option **)
+    
+    let fixpoint successors topnode transf entrypoints =
+!     let pred = make_predecessors successors topnode in
+!     DS.fixpoint (fun s -> Maps.PMap.get s pred) topnode transf entrypoints
+   end
+  
+  module type ORDERED_TYPE_WITH_TOP = 
diff --git a/extraction/Linearize.ml.patch b/extraction/Linearize.ml.patch
new file mode 100644
index 0000000..47b6cc9
--- /dev/null
+++ b/extraction/Linearize.ml.patch
@@ -0,0 +1,22 @@
+*** Linearize.ml.orig	2006-02-09 11:47:55.000000000 +0100
+--- Linearize.ml	2006-02-09 11:58:42.000000000 +0100
+***************
+*** 28,35 ****
+  (** val enumerate : LTL.coq_function -> node list **)
+  
+  let enumerate f =
+    positive_rec Coq_nil (fun pc nodes ->
+!     match Maps.PMap.get pc (reachable f) with
+        | true -> Coq_cons (pc, nodes)
+        | false -> nodes) (coq_Psucc f.fn_entrypoint)
+  
+--- 28,36 ----
+  (** val enumerate : LTL.coq_function -> node list **)
+  
+  let enumerate f =
++   let reach = reachable f in
+    positive_rec Coq_nil (fun pc nodes ->
+!     match Maps.PMap.get pc reach with
+        | true -> Coq_cons (pc, nodes)
+        | false -> nodes) (coq_Psucc f.fn_entrypoint)
+  
diff --git a/extraction/Makefile b/extraction/Makefile
new file mode 100644
index 0000000..038b3d0
--- /dev/null
+++ b/extraction/Makefile
@@ -0,0 +1,91 @@
+FILES=\
+  Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \
+  Bool.ml List.ml Sumbool.ml BinPos.ml BinNat.ml BinInt.ml \
+  ZArith_dec.ml Zeven.ml Zmin.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \
+  FSetInterface.ml FSetBridge.ml FSetList.ml FSetAVL.ml \
+  Coqlib.ml Maps.ml Sets.ml union_find.ml AST.ml Integers.ml \
+  ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Values.ml \
+  Mem.ml Globalenvs.ml \
+  Op.ml Cminor.ml Cmconstr.ml \
+  Csharpminor.ml Cminorgen.ml \
+  Registers.ml RTL.ml \
+  ../caml/RTLgenaux.ml RTLgen.ml \
+  RTLtyping.ml \
+  Lattice.ml Kildall.ml \
+  Constprop.ml CSE.ml \
+  Locations.ml Conventions.ml LTL.ml \
+  Ordered.ml InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \
+  Parallelmove.ml Allocation.ml  \
+  Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \
+  Mach.ml Stacking.ml \
+  PPC.ml PPCgen.ml \
+  Main.ml \
+  ../caml/CMparser.ml ../caml/CMlexer.ml \
+  ../caml/PrintPPC.ml ../caml/Main2.ml
+
+EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES))
+GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli)
+
+CAMLINCL=-I ../caml
+OCAMLC=ocamlc -g $(CAMLINCL)
+OCAMLOPT=ocamlopt $(CAMLINCL)
+OCAMLDEP=ocamldep $(CAMLINCL)
+
+COQINCL=-I ../lib -I ../backend
+COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source
+
+../ccomp: $(FILES:.ml=.cmo)
+	$(OCAMLC) -o ../ccomp $(FILES:.ml=.cmo)
+
+../ccomp.opt: Pack.cmx
+	$(OCAMLOPT) -o ../ccomp.opt Pack.cmx
+
+Pack.cmx: $(FILES:.ml=.cmx)
+	$(OCAMLOPT) -pack -o Pack.cmx $(FILES:.ml=.cmx)
+
+extraction:
+	@rm -f $(GENFILES)
+	$(COQEXEC) extraction.v
+	@echo "Fixing file names..."
+	@for i in $(GENFILES); do \
+          j=`./uncapitalize $$i`; \
+          test -f $$i || (test -f $$j && mv $$j $$i); \
+         done
+	@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
+
+.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
+	rm -f ccomp
+
+depend: beforedepend
+	$(OCAMLDEP) ../caml/*.mli ../caml/*.ml *.mli *.ml > .depend
+
+include .depend
+
+
diff --git a/extraction/extraction.v b/extraction/extraction.v
new file mode 100644
index 0000000..1717882
--- /dev/null
+++ b/extraction/extraction.v
@@ -0,0 +1,53 @@
+Require Floats.
+Require Kildall.
+Require RTLgen.
+Require Coloring.
+Require Allocation.
+Require Cmconstr.
+Require Main.
+
+(* Standard lib *)
+Extract Inductive unit => "unit" [ "()" ].
+Extract Inductive bool => "bool" [ "true" "false" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
+
+(* Float *)
+Extract Inlined Constant Floats.float => "float".
+Extract Constant Floats.Float.zero   => "0.".
+Extract Constant Floats.Float.one   => "1.".
+Extract Constant Floats.Float.neg => "( ~-. )".
+Extract Constant Floats.Float.abs => "abs_float".
+Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat".
+Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat".
+Extract Constant Floats.Float.floatofint => "Floataux.floatofint".
+Extract Constant Floats.Float.floatofintu => "Floataux.floatofintu".
+Extract Constant Floats.Float.add => "( +. )".
+Extract Constant Floats.Float.sub => "( -. )".
+Extract Constant Floats.Float.mul => "( *. )".
+Extract Constant Floats.Float.div => "( /. )".
+Extract Constant Floats.Float.cmp => "Floataux.cmp".
+Extract Constant Floats.Float.eq_dec => "fun (x: float) (y: float) -> x = y".
+
+(* RTLgen *)
+Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".
+
+(* Coloring *)
+Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
+
+(* PPC *)
+Extract Constant PPC.low_half_signed => "fun _ -> assert false".
+Extract Constant PPC.high_half_signed => "fun _ -> assert false".
+Extract Constant PPC.low_half_unsigned => "fun _ -> assert false".
+Extract Constant PPC.high_half_unsigned => "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".
+
+(* Go! *)
+Recursive Extraction Library Main.
+(*Extraction Library Compare_dec.
+  Extraction Library Cmconstr.*)
diff --git a/extraction/uncapitalize b/extraction/uncapitalize
new file mode 100755
index 0000000..d724b8f
--- /dev/null
+++ b/extraction/uncapitalize
@@ -0,0 +1,6 @@
+#!/bin/sh
+echo $1 | sed -e 'h
+s/\(.\).*/\1/
+y/ABCDEFGHIJKLMNOPQRSTUVWXYZ/abcdefghijklmnopqrstuvwxyz/
+G
+s/\n.//'