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, 39 insertions, 31 deletions

diff --git a/.depend b/.depend
index dc2aa64..c35ce16 100644
--- a/.depend
+++ b/.depend
@@ -5,60 +5,68 @@ lib/union_find.vo: lib/union_find.v
 lib/Inclusion.vo: lib/Inclusion.v
 lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo
 lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo
-lib/Integers.vo: lib/Integers.v lib/Coqlib.vo backend/AST.vo
-lib/Floats.vo: lib/Floats.v backend/AST.vo lib/Integers.vo
-backend/AST.vo: backend/AST.v lib/Coqlib.vo
+lib/Iteration.vo: lib/Iteration.v lib/Coqlib.vo
+lib/Integers.vo: lib/Integers.v lib/Coqlib.vo
+lib/Floats.vo: lib/Floats.v lib/Integers.vo
+lib/Parmov.vo: lib/Parmov.v lib/Coqlib.vo
+backend/AST.vo: backend/AST.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo
 backend/Values.vo: backend/Values.v lib/Coqlib.vo backend/AST.vo lib/Integers.vo lib/Floats.vo
 backend/Mem.vo: backend/Mem.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo
+backend/Events.vo: backend/Events.v lib/Coqlib.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo
 backend/Globalenvs.vo: backend/Globalenvs.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo
 backend/Op.vo: backend/Op.v lib/Coqlib.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo
-backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Op.vo backend/Globalenvs.vo
+backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Events.vo backend/Values.vo backend/Mem.vo backend/Op.vo backend/Globalenvs.vo
 backend/Cmconstr.vo: backend/Cmconstr.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Op.vo backend/Globalenvs.vo backend/Cminor.vo
-backend/Cmconstrproof.vo: backend/Cmconstrproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Op.vo backend/Globalenvs.vo backend/Cminor.vo backend/Cmconstr.vo
-backend/Csharpminor.vo: backend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo
+backend/Cmconstrproof.vo: backend/Cmconstrproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Op.vo backend/Globalenvs.vo backend/Cminor.vo backend/Cmconstr.vo
+backend/Csharpminor.vo: backend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo
 backend/Cminorgen.vo: backend/Cminorgen.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo backend/AST.vo lib/Integers.vo backend/Mem.vo backend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo
-backend/Cminorgenproof.vo: backend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo backend/Cminorgen.vo backend/Cmconstrproof.vo
+backend/Cminorgenproof.vo: backend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo backend/Cminorgen.vo backend/Cmconstrproof.vo
 backend/Registers.vo: backend/Registers.v lib/Coqlib.vo backend/AST.vo lib/Maps.vo lib/Sets.vo
-backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo
+backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo
 backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo
-backend/RTLgenproof1.vo: backend/RTLgenproof1.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo
-backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenproof1.vo
-backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/union_find.vo backend/Globalenvs.vo backend/Values.vo backend/Mem.vo lib/Integers.vo
-backend/Kildall.vo: backend/Kildall.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo
+backend/RTLgenproof1.vo: backend/RTLgenproof1.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo
+backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenproof1.vo
+backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Globalenvs.vo backend/Values.vo backend/Mem.vo lib/Integers.vo backend/Events.vo
+backend/Kildall.vo: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo
 backend/Constprop.vo: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo
-backend/Constpropproof.vo: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Constprop.vo
+backend/Constpropproof.vo: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Constprop.vo
 backend/CSE.vo: backend/CSE.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo
-backend/CSEproof.vo: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo
+backend/CSEproof.vo: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo
 backend/Locations.vo: backend/Locations.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo
 backend/Conventions.vo: backend/Conventions.v lib/Coqlib.vo backend/AST.vo backend/Locations.vo
-backend/LTL.vo: backend/LTL.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo
+backend/LTL.vo: backend/LTL.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo
 backend/LTLtyping.vo: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
 backend/InterfGraph.vo: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo
 backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo
 backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo
-backend/Parallelmove.vo: backend/Parallelmove.v backend/Conventions.vo lib/Coqlib.vo backend/Values.vo backend/LTL.vo backend/Locations.vo backend/AST.vo
+backend/Parallelmove.vo: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo backend/Values.vo backend/Events.vo backend/AST.vo backend/Locations.vo backend/Conventions.vo
 backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Parallelmove.vo backend/LTL.vo
-backend/Allocproof_aux.vo: backend/Allocproof_aux.v lib/Coqlib.vo backend/Values.vo backend/Parallelmove.vo backend/Allocation.vo backend/LTL.vo backend/Locations.vo backend/Conventions.vo
-backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof_aux.vo backend/LTL.vo
-backend/Alloctyping_aux.vo: backend/Alloctyping_aux.v lib/Coqlib.vo backend/Locations.vo backend/LTL.vo backend/Allocation.vo backend/LTLtyping.vo backend/Allocproof_aux.vo backend/Parallelmove.vo lib/Inclusion.vo
-backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo backend/Alloctyping_aux.vo
+backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Parallelmove.vo backend/Allocation.vo backend/LTL.vo
+backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo backend/Parallelmove.vo
 backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo
-backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
+backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
 backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo
-backend/Linear.vo: backend/Linear.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
+backend/Linear.vo: backend/Linear.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
 backend/Lineartyping.vo: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo
 backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo backend/AST.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Kildall.vo lib/Lattice.vo
-backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo lib/Lattice.vo
+backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo lib/Lattice.vo
 backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo backend/LTLtyping.vo backend/Lineartyping.vo backend/Conventions.vo
-backend/Mach.vo: backend/Mach.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo
-backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Mem.vo lib/Integers.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo
-backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Mem.vo lib/Integers.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo
+backend/Mach.vo: backend/Mach.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo
+backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Mem.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo
+backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Mem.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo
 backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Conventions.vo
-backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Op.vo backend/Mem.vo backend/Globalenvs.vo backend/Locations.vo backend/Mach.vo backend/Machabstr.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Stacking.vo
+backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Op.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Locations.vo backend/Mach.vo backend/Machabstr.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Stacking.vo
 backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo backend/AST.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Stacking.vo backend/Stackingproof.vo
-backend/Machabstr2mach.vo: backend/Machabstr2mach.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Machabstr.vo backend/Mach.vo backend/Machtyping.vo backend/Stackingproof.vo
-backend/PPC.vo: backend/PPC.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo
+backend/Machabstr2mach.vo: backend/Machabstr2mach.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Machabstr.vo backend/Mach.vo backend/Machtyping.vo backend/Stackingproof.vo
+backend/PPC.vo: backend/PPC.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo
 backend/PPCgen.vo: backend/PPCgen.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/PPC.vo
-backend/PPCgenproof1.vo: backend/PPCgenproof1.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo
-backend/PPCgenproof.vo: backend/PPCgenproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo backend/PPCgenproof1.vo
+backend/PPCgenproof1.vo: backend/PPCgenproof1.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo backend/Conventions.vo
+backend/PPCgenproof.vo: backend/PPCgenproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo backend/PPCgenproof1.vo
 backend/Main.vo: backend/Main.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Csharpminor.vo backend/Cminor.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo backend/PPC.vo backend/Cminorgen.vo backend/RTLgen.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Stacking.vo backend/PPCgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Lineartyping.vo backend/Machtyping.vo backend/Cminorgenproof.vo backend/RTLgenproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2mach.vo backend/PPCgenproof.vo
+cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo backend/AST.vo
+cfrontend/Csem.vo: cfrontend/Csem.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/AST.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo cfrontend/Csyntax.vo
+cfrontend/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo cfrontend/Csyntax.vo
+cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo backend/AST.vo cfrontend/Csyntax.vo backend/Csharpminor.vo
+cfrontend/Cshmgenproof1.vo: cfrontend/Cshmgenproof1.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/AST.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo backend/Csharpminor.vo cfrontend/Cshmgen.vo
+cfrontend/Cshmgenproof2.vo: cfrontend/Cshmgenproof2.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/AST.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo backend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo
+cfrontend/Cshmgenproof3.vo: cfrontend/Cshmgenproof3.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/AST.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo backend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo cfrontend/Cshmgenproof2.vo