Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


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

1 files changed, 7 insertions, 6 deletions

diff --git a/extraction/Makefile b/extraction/Makefile
index 687c5c52..6ae8e35d 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -1,19 +1,20 @@
 FILES=\
   Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \
   Bool.ml CList.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 \
+  ZArith_dec.ml Zeven.ml Zmax.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \
+  Int.ml OrderedType.ml FSetList.ml FSetAVL.ml \
+  Coqlib.ml Maps.ml Sets.ml AST.ml Iteration.ml Integers.ml \
+  ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.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 \
+  Locations.ml Conventions.ml \
+  ../caml/RTLtypingaux.ml RTLtyping.ml \
   Lattice.ml Kildall.ml \
   Constprop.ml CSE.ml \
-  Locations.ml Conventions.ml LTL.ml \
+  LTL.ml \
   Ordered.ml InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \
   Parallelmove.ml Allocation.ml  \
   Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \