From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: 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 --- .depend | 70 ++++++++++++++++++++++++++++++++++++----------------------------- 1 file changed, 39 insertions(+), 31 deletions(-) (limited to '.depend') 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 -- cgit v1.2.3