diff options
85 files changed, 73 insertions, 235 deletions
@@ -15,110 +15,110 @@ lib/Postorder.vo lib/Postorder.glob: lib/Postorder.v lib/Coqlib.vo lib/Maps.vo l common/Errors.vo common/Errors.glob: common/Errors.v lib/Coqlib.vo common/AST.vo common/AST.glob: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Events.glob: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Errors.vo -common/Globalenvs.vo common/Globalenvs.glob: common/Globalenvs.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo +common/Globalenvs.vo common/Globalenvs.glob: common/Globalenvs.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Memdata.vo common/Memdata.glob: common/Memdata.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memtype.vo common/Memtype.glob: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Memory.glob: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo lib/Intv.vo common/Values.vo common/Values.glob: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo -common/Smallstep.vo common/Smallstep.glob: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo -common/Behaviors.vo common/Behaviors.glob: common/Behaviors.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo +common/Smallstep.vo common/Smallstep.glob: common/Smallstep.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo +common/Behaviors.vo common/Behaviors.glob: common/Behaviors.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo common/Switch.vo common/Switch.glob: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo -common/Determinism.vo common/Determinism.glob: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo +common/Determinism.vo common/Determinism.glob: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo backend/Cminor.vo backend/Cminor.glob: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo -$(ARCH)/Op.vo $(ARCH)/Op.glob: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo common/Events.vo -backend/CminorSel.vo backend/CminorSel.glob: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo -$(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob: $(ARCH)/SelectOp.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo -backend/Selection.vo backend/Selection.glob: backend/Selection.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo -$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo -backend/Selectionproof.vo backend/Selectionproof.glob: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo +$(ARCH)/Op.vo $(ARCH)/Op.glob: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo +backend/CminorSel.vo backend/CminorSel.glob: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo +$(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob: $(ARCH)/SelectOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo +backend/Selection.vo backend/Selection.glob: backend/Selection.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +backend/Selectionproof.vo backend/Selectionproof.glob: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/Registers.vo backend/Registers.glob: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo backend/RTL.vo backend/RTL.glob: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo -backend/RTLgen.vo backend/RTLgen.glob: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo -backend/RTLgenspec.vo backend/RTLgenspec.glob: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo +backend/RTLgen.vo backend/RTLgen.glob: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo +backend/RTLgenspec.vo backend/RTLgenspec.glob: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenproof.vo backend/RTLgenproof.glob: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo -backend/Tailcall.vo backend/Tailcall.glob: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo +backend/Tailcall.vo backend/Tailcall.glob: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo backend/Tailcallproof.vo backend/Tailcallproof.glob: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo -backend/Inlining.vo backend/Inlining.glob: backend/Inlining.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo -backend/Inliningspec.vo backend/Inliningspec.glob: backend/Inliningspec.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo +backend/Inlining.vo backend/Inlining.glob: backend/Inlining.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo +backend/Inliningspec.vo backend/Inliningspec.glob: backend/Inliningspec.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo backend/Inliningproof.vo backend/Inliningproof.glob: backend/Inliningproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/Inlining.vo backend/Inliningspec.vo backend/RTL.vo -backend/Renumber.vo backend/Renumber.glob: backend/Renumber.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/AST.vo backend/RTL.vo -backend/Renumberproof.vo backend/Renumberproof.glob: backend/Renumberproof.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Renumber.vo -backend/RTLtyping.vo backend/RTLtyping.glob: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Memory.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo backend/Conventions.vo +backend/Renumber.vo backend/Renumber.glob: backend/Renumber.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo backend/RTL.vo +backend/Renumberproof.vo backend/Renumberproof.glob: backend/Renumberproof.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Renumber.vo +backend/RTLtyping.vo backend/RTLtyping.glob: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Events.vo backend/RTL.vo backend/Conventions.vo backend/Kildall.vo backend/Kildall.glob: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo -$(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo -backend/Constprop.vo backend/Constprop.glob: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo +$(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo +backend/Constprop.vo backend/Constprop.glob: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo -backend/Constpropproof.vo backend/Constpropproof.glob: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo +backend/Constpropproof.vo backend/Constpropproof.glob: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo $(ARCH)/SelectOp.vo -backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo +backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo -backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo +backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo $(ARCH)/Machregs.vo $(ARCH)/Machregs.glob: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo -backend/Locations.vo backend/Locations.glob: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo +backend/Locations.vo backend/Locations.glob: backend/Locations.v lib/Coqlib.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo backend/Conventions.vo backend/Conventions.glob: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo backend/LTL.vo backend/LTL.glob: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo -backend/LTLtyping.vo backend/LTLtyping.glob: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/InterfGraph.vo backend/InterfGraph.glob: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo +backend/LTLtyping.vo backend/LTLtyping.glob: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo +backend/InterfGraph.vo backend/InterfGraph.glob: backend/InterfGraph.v lib/Coqlib.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo backend/Coloring.vo backend/Coloring.glob: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/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.glob: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo -backend/Allocation.vo backend/Allocation.glob: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/LTL.vo +backend/Allocation.vo backend/Allocation.glob: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Coloring.vo backend/LTL.vo backend/Allocproof.vo backend/Allocproof.glob: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/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/LTL.vo backend/Alloctyping.vo backend/Alloctyping.glob: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/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/Tunneling.vo backend/Tunneling.glob: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo +backend/Tunneling.vo backend/Tunneling.glob: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo backend/Tunnelingproof.vo backend/Tunnelingproof.glob: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo -backend/Tunnelingtyping.vo backend/Tunnelingtyping.glob: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo -backend/LTLin.vo backend/LTLin.glob: backend/LTLin.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/LTLintyping.vo backend/LTLintyping.glob: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.vo backend/Conventions.vo -backend/Linearize.vo backend/Linearize.glob: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Errors.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo +backend/Tunnelingtyping.vo backend/Tunnelingtyping.glob: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo +backend/LTLin.vo backend/LTLin.glob: backend/LTLin.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo +backend/LTLintyping.vo backend/LTLintyping.glob: backend/LTLintyping.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.vo backend/Conventions.vo +backend/Linearize.vo backend/Linearize.glob: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Errors.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo backend/Linearizeproof.vo backend/Linearizeproof.glob: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo backend/Linearizetyping.vo backend/Linearizetyping.glob: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo -backend/CleanupLabels.vo backend/CleanupLabels.glob: backend/CleanupLabels.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/LTLin.vo -backend/CleanupLabelsproof.vo backend/CleanupLabelsproof.glob: backend/CleanupLabelsproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/CleanupLabels.vo -backend/CleanupLabelstyping.vo backend/CleanupLabelstyping.glob: backend/CleanupLabelstyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/CleanupLabels.vo backend/LTLintyping.vo -backend/Linear.vo backend/Linear.glob: backend/Linear.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/Lineartyping.vo backend/Lineartyping.glob: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Conventions.vo -backend/Parallelmove.vo backend/Parallelmove.glob: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo -backend/Reload.vo backend/Reload.glob: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo backend/Parallelmove.vo backend/Linear.vo -backend/Reloadproof.vo backend/Reloadproof.glob: backend/Reloadproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Parallelmove.vo backend/Reload.vo -backend/Reloadtyping.vo backend/Reloadtyping.glob: backend/Reloadtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo -backend/RRE.vo backend/RRE.glob: backend/RRE.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo -backend/RREproof.vo backend/RREproof.glob: backend/RREproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/RRE.vo +backend/CleanupLabels.vo backend/CleanupLabels.glob: backend/CleanupLabels.v lib/Coqlib.vo lib/Ordered.vo backend/LTLin.vo +backend/CleanupLabelsproof.vo backend/CleanupLabelsproof.glob: backend/CleanupLabelsproof.v lib/Coqlib.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/CleanupLabels.vo +backend/CleanupLabelstyping.vo backend/CleanupLabelstyping.glob: backend/CleanupLabelstyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/CleanupLabels.vo backend/LTLintyping.vo +backend/Linear.vo backend/Linear.glob: backend/Linear.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo +backend/Lineartyping.vo backend/Lineartyping.glob: backend/Lineartyping.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Conventions.vo +backend/Parallelmove.vo backend/Parallelmove.glob: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/AST.vo backend/Locations.vo backend/Conventions.vo +backend/Reload.vo backend/Reload.glob: backend/Reload.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo backend/Parallelmove.vo backend/Linear.vo +backend/Reloadproof.vo backend/Reloadproof.glob: backend/Reloadproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Parallelmove.vo backend/Reload.vo +backend/Reloadtyping.vo backend/Reloadtyping.glob: backend/Reloadtyping.v lib/Coqlib.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo +backend/RRE.vo backend/RRE.glob: backend/RRE.v lib/Coqlib.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo +backend/RREproof.vo backend/RREproof.glob: backend/RREproof.v lib/Axioms.vo lib/Coqlib.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/RRE.vo backend/RREtyping.vo backend/RREtyping.glob: backend/RREtyping.v lib/Coqlib.vo common/AST.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/RRE.vo backend/RREproof.vo -backend/Mach.vo backend/Mach.glob: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo -backend/Machtyping.vo backend/Machtyping.glob: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo -backend/Bounds.vo backend/Bounds.glob: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo +backend/Mach.vo backend/Mach.glob: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo +backend/Machtyping.vo backend/Machtyping.glob: backend/Machtyping.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo +backend/Bounds.vo backend/Bounds.glob: backend/Bounds.v lib/Coqlib.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob: $(ARCH)/$(VARIANT)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo -backend/Stacking.vo backend/Stacking.glob: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo -backend/Stackingproof.vo backend/Stackingproof.glob: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machsem.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo -backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo -backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo +backend/Stacking.vo backend/Stacking.glob: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo +backend/Stackingproof.vo backend/Stackingproof.glob: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machsem.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo +backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo +backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo -$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo -$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo +$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo cfrontend/Ctypes.vo cfrontend/Ctypes.glob: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo cfrontend/Cop.vo cfrontend/Cop.glob: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo -cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo +cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo common/Smallstep.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo -cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo -cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo -cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo -cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo +cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo +cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo +cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo -cfrontend/ClightBigstep.vo cfrontend/ClightBigstep.glob: cfrontend/ClightBigstep.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo -cfrontend/SimplLocals.vo cfrontend/SimplLocals.glob: cfrontend/SimplLocals.v lib/Coqlib.vo lib/Ordered.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo +cfrontend/ClightBigstep.vo cfrontend/ClightBigstep.glob: cfrontend/ClightBigstep.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo +cfrontend/SimplLocals.vo cfrontend/SimplLocals.glob: cfrontend/SimplLocals.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo cfrontend/SimplLocalsproof.vo cfrontend/SimplLocalsproof.glob: cfrontend/SimplLocalsproof.v lib/Coqlib.vo common/Errors.vo lib/Ordered.vo common/AST.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo -cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo -cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo -driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/RRE.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.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/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/RREproof.vo backend/RREtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo +cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo cfrontend/Csharpminor.vo backend/Cminor.vo +cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo +driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/RRE.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.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/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/RREproof.vo backend/RREtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_float_prop.glob: flocq/Core/Fcore_float_prop.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.glob: flocq/Core/Fcore_Zaux.v diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 4200c11..b78dfb6 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -13,14 +13,10 @@ (** Translation from Mach to ARM. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v index 48b6328..2d3c72d 100644 --- a/arm/Asmgenretaddr.v +++ b/arm/Asmgenretaddr.v @@ -17,13 +17,9 @@ return addresses that are stored in activation records. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 0f06703..a9cbad5 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -17,7 +17,6 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. Require Import Op. Require Import Registers. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 0cee786..6415248 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -640,7 +640,8 @@ let print_instruction oc = function | EF_inline_asm txt -> fprintf oc "%s begin inline assembly\n" comment; fprintf oc " %s\n" (extern_atom txt); - fprintf oc "%s end inline assembly\n" comment + fprintf oc "%s end inline assembly\n" comment; + 5 (* hoping this is an upper bound... *) | _ -> assert false end @@ -754,13 +755,13 @@ let print_var oc name v = fprintf oc " .size %a, . - %a\n" print_symb name print_symb name let print_globdef oc (name, gdef) = + match gdef with | Gfun(Internal f) -> print_function oc name f | Gfun(External ef) -> () | Gvar v -> print_var oc name v let print_program oc p = (* fprintf oc " .fpu vfp\n"; *) - List.iter (print_var oc) p.prog_vars; List.iter (print_globdef oc) p.prog_defs diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 255c97c..22ef88d 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -37,14 +37,9 @@ *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Cminor. Require Import Op. Require Import CminorSel. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index a72913d..e25fb0c 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -19,9 +19,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. -Require Import Events. Require Import Globalenvs. -Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. diff --git a/backend/Allocation.v b/backend/Allocation.v index 508bc13..4a4c219 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -17,16 +17,12 @@ Require Import Errors. Require Import Maps. Require Import Lattice. Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. Require Import RTLtyping. Require Import Kildall. Require Import Locations. -Require Import Conventions. Require Import Coloring. (** * Liveness analysis over RTL *) diff --git a/backend/Allocproof.v b/backend/Allocproof.v index a9477e0..2011485 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -14,7 +14,6 @@ RTL to LTL). *) Require Import FSets. -Require Import SetoidList. Require Import Coqlib. Require Import Errors. Require Import Maps. diff --git a/backend/Bounds.v b/backend/Bounds.v index 23fa3b5..ef78b2e 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -13,7 +13,6 @@ (** Computation of resource bounds for Linear code. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Op. Require Import Locations. diff --git a/backend/CSE.v b/backend/CSE.v index 85f46e2..1888fb8 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -21,7 +21,6 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 49b213b..5569123 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -16,8 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Errors. -Require Import Integers. -Require Import Floats. Require Import Values. Require Import Memory. Require Import Events. diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v index 7401abc..0ed2be1 100644 --- a/backend/CleanupLabels.v +++ b/backend/CleanupLabels.v @@ -21,7 +21,6 @@ branched to. *) Require Import Coqlib. -Require Import Maps. Require Import Ordered. Require Import FSets. Require FSetAVL. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index a7a60f6..dbd33c1 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -13,7 +13,6 @@ (** Correctness proof for clean-up of labels *) Require Import Coqlib. -Require Import Maps. Require Import Ordered. Require Import FSets. Require Import AST. @@ -22,7 +21,6 @@ Require Import Values. Require Import Memory. Require Import Events. Require Import Globalenvs. -Require Import Errors. Require Import Smallstep. Require Import Op. Require Import Locations. diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v index ea9de86..f58a910 100644 --- a/backend/CleanupLabelstyping.v +++ b/backend/CleanupLabelstyping.v @@ -14,7 +14,6 @@ Require Import Coqlib. Require Import Maps. -Require Import Errors. Require Import AST. Require Import Op. Require Import Locations. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index a063544..b5a0d39 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -16,7 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. Require Import Events. Require Import Values. Require Import Memory. diff --git a/backend/Constprop.v b/backend/Constprop.v index fc242e1..fe16240 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -19,8 +19,6 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index f14e87a..1b90666 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -16,7 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. Require Import Values. Require Import Events. Require Import Memory. diff --git a/backend/Inlining.v b/backend/Inlining.v index 3ddfe9a..5075fd6 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -18,7 +18,6 @@ Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. Require Import Op. Require Import Registers. Require Import RTL. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 84bcdcd..014986d 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -18,7 +18,6 @@ Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. Require Import Globalenvs. Require Import Op. Require Import Registers. diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index ec64e99..9a5522d 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -15,7 +15,6 @@ Require Import Coqlib. Require Import FSets. Require Import FSetAVL. -Require Import Maps. Require Import Ordered. Require Import Registers. Require Import Locations. diff --git a/backend/LTLin.v b/backend/LTLin.v index 390c4cf..e0d5ca2 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -17,7 +17,6 @@ instructions with explicit labels and ``goto'' instructions. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. @@ -28,7 +27,6 @@ Require Import Smallstep. Require Import Op. Require Import Locations. Require Import LTL. -Require Import Conventions. (** * Abstract syntax *) diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index e9cc2df..0338667 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -13,12 +13,9 @@ (** Typing rules for LTLin. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. -Require Import Memdata. Require Import Op. -Require Import RTL. Require Import Locations. Require Import LTLin. Require LTLtyping. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 2e627e9..0c90514 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -16,9 +16,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Memdata. Require Import Op. -Require Import RTL. Require Import Locations. Require Import LTL. Require Import Conventions. diff --git a/backend/Linear.v b/backend/Linear.v index b218531..52f5fd7 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -18,7 +18,6 @@ [Lsetstack] are provided to access stack slots. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. diff --git a/backend/Linearize.v b/backend/Linearize.v index fd350c7..636cb22 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -19,8 +19,6 @@ Require Import Ordered. Require Import FSets. Require FSetAVL. Require Import AST. -Require Import Values. -Require Import Globalenvs. Require Import Errors. Require Import Op. Require Import Locations. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index da73b00..32d6045 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -13,7 +13,6 @@ (** Typing rules for Linear. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. diff --git a/backend/Locations.v b/backend/Locations.v index 0b538fd..ba2fb06 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -14,7 +14,6 @@ the results of register allocation (file [Allocation]). *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Values. Require Export Machregs. diff --git a/backend/Mach.v b/backend/Mach.v index 669d35e..56c0369 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -21,10 +21,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Memory. -Require Import Events. Require Import Globalenvs. -Require Import Smallstep. Require Import Op. Require Import Locations. Require Import Conventions. diff --git a/backend/Machsem.v b/backend/Machsem.v index a802323..6d5f1cf 100644 --- a/backend/Machsem.v +++ b/backend/Machsem.v @@ -13,7 +13,6 @@ (** The Mach intermediate language: operational semantics. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. diff --git a/backend/Machtyping.v b/backend/Machtyping.v index b9d8009..2dc19be 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -13,14 +13,8 @@ (** Type system for the Mach intermediate language. *) Require Import Coqlib. -Require Import Maps. Require Import AST. -Require Import Memory. Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Conventions. diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index d7a4217..4930ccd 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.v @@ -24,7 +24,6 @@ Require Import Coqlib. Require Parmov. Require Import Values. -Require Import Events. Require Import AST. Require Import Locations. Require Import Conventions. diff --git a/backend/RRE.v b/backend/RRE.v index 95eadce..ece6051 100644 --- a/backend/RRE.v +++ b/backend/RRE.v @@ -13,10 +13,7 @@ (** Redundant Reloads Elimination *) Require Import Coqlib. -Require Import Maps. Require Import AST. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Conventions. diff --git a/backend/RREproof.v b/backend/RREproof.v index d70a1fd..8926fe4 100644 --- a/backend/RREproof.v +++ b/backend/RREproof.v @@ -14,7 +14,6 @@ Require Import Axioms. Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Values. Require Import Globalenvs. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 62df254..007191a 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -17,7 +17,6 @@ Require Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. Require Import Switch. Require Import Op. Require Import Registers. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 1b8e853..690611c 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -617,9 +617,10 @@ Proof. edestruct Mem.loadv_extends as [v' []]; eauto. exists (rs1#rd <- v'). (* Exec *) - split. eapply star_right. eexact EX1. eapply exec_Iload; eauto. - rewrite (@eval_addressing_preserved _ _ _ _ ge tge). eauto. - exact symbols_preserved. traceEq. + split. eapply star_right. eexact EX1. eapply exec_Iload. eauto. + instantiate (1 := vaddr'). rewrite <- H3. + apply eval_addressing_preserved. exact symbols_preserved. + auto. traceEq. (* Match-env *) split. eauto with rtlg. (* Result *) @@ -1049,9 +1050,9 @@ Proof. edestruct Mem.storev_extends as [tm' []]; eauto. econstructor; split. left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. - eapply exec_Istore with (a := vaddr'); eauto. + eapply exec_Istore with (a := vaddr'). eauto. rewrite <- H4. apply eval_addressing_preserved. exact symbols_preserved. - traceEq. + eauto. traceEq. econstructor; eauto. constructor. (* call *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 5114390..c50c702 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -25,10 +25,6 @@ Require Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. -Require Import Events. -Require Import Memory. -Require Import Globalenvs. Require Import Switch. Require Import Op. Require Import Registers. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index a14e944..f8dbfe4 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -20,10 +20,8 @@ Require Import Op. Require Import Registers. Require Import Globalenvs. Require Import Values. -Require Import Memory. Require Import Integers. Require Import Events. -Require Import Smallstep. Require Import RTL. Require Import Conventions. diff --git a/backend/Registers.v b/backend/Registers.v index fceb7c2..47e10fa 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -21,7 +21,6 @@ Require Import Coqlib. Require Import AST. Require Import Maps. Require Import Ordered. -Require Import FSets. Require FSetAVL. Definition reg: Type := positive. diff --git a/backend/Reload.v b/backend/Reload.v index 0ad53e6..31bddcd 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -13,11 +13,8 @@ (** Reloading, spilling, and explication of calling conventions. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import LTLin. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 75c7dad..1d49909 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -13,7 +13,6 @@ (** Correctness proof for the [Reload] pass. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. @@ -24,7 +23,6 @@ Require Import Smallstep. Require Import Op. Require Import Locations. Require Import Conventions. -Require Import Allocproof. Require Import RTLtyping. Require Import LTLin. Require Import LTLintyping. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index eba5ad6..99c89ab 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -14,7 +14,6 @@ correctness of computation of stack bounds for Linear. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Op. Require Import Locations. diff --git a/backend/Renumber.v b/backend/Renumber.v index b933bba..c862318 100644 --- a/backend/Renumber.v +++ b/backend/Renumber.v @@ -15,7 +15,6 @@ Require Import Coqlib. Require Import Maps. Require Import Postorder. -Require Import AST. Require Import RTL. (** CompCert's dataflow analyses (module [Kildall]) are more precise diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 5ec29e2..d086010 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -15,10 +15,7 @@ Require Import Coqlib. Require Import Maps. Require Import Postorder. -Require Import AST. -Require Import Values. Require Import Events. -Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Op. diff --git a/backend/Selection.v b/backend/Selection.v index ff4d863..29bdabc 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -23,12 +23,8 @@ The source language is Cminor and the target language is CminorSel. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. Require Import Globalenvs. Require Cminor. Require Import Op. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 2fd9219..09dc0ff 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -16,7 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. Require Import Values. Require Import Memory. Require Import Events. diff --git a/backend/Stacking.v b/backend/Stacking.v index 23a112c..732443b 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -13,12 +13,10 @@ (** Layout of activation records; translation from Linear to Mach. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. Require Import Op. -Require Import RTL. Require Import Locations. Require Import Linear. Require Import Bounds. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1d87ad3..6c4e43f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -15,7 +15,6 @@ (** This file proves semantic preservation for the [Stacking] pass. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index 27de557..2324cd5 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -13,7 +13,6 @@ (** Type preservation for the [Stacking] pass. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import Integers. Require Import AST. diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 158002e..917ec83 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -15,7 +15,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. -Require Import Globalenvs. Require Import Registers. Require Import Op. Require Import RTL. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 8dd1fe2..18414a8 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -16,10 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import UnionFind. Require Import AST. -Require Import Values. -Require Import Globalenvs. -Require Import Op. -Require Import Locations. Require Import LTL. (** Branch tunneling shortens sequences of branches (with no intervening diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index 743b468..dfc36b6 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -14,13 +14,7 @@ Require Import Coqlib. Require Import Maps. -Require Import UnionFind. Require Import AST. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Op. -Require Import Locations. Require Import LTL. Require Import LTLtyping. Require Import Tunneling. diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 293ea5d..4d10c62 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -16,7 +16,6 @@ (** A big-step semantics for the Clight language. *) Require Import Coqlib. -Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index e024caf..af85971 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -23,7 +23,6 @@ Require Import Ordered. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Memdata. Require Import Csharpminor. Require Import Cminor. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 018fcec..62690d6 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -23,7 +23,6 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Memdata. Require Import Memory. Require Import Events. Require Import Globalenvs. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 0d2f235..b28409d 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -15,7 +15,6 @@ (** A deterministic evaluation strategy for C. *) -Require Import Coq.Program.Equality. Require Import Axioms. Require Import Coqlib. Require Import Errors. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 5155689..6c333aa 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -16,7 +16,6 @@ (** Abstract syntax for the Compcert C language *) Require Import Coqlib. -Require Import Errors. Require Import Integers. Require Import Floats. Require Import Values. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 641ea3c..8757ba2 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -22,7 +22,6 @@ Require Import Memory. Require Import Ctypes. Require Import Cop. Require Import Csyntax. -Require Import Csem. Open Scope error_monad_scope. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 153f177..ab35445 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -22,8 +22,6 @@ Require Import AST. Require Import Ctypes. Require Import Cop. Require Import Csyntax. -Require Import Csem. -Require Cstrategy. Require Import Clight. Module C := Csyntax. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 7fc0a46..59fc9bc 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -12,8 +12,6 @@ (** Correctness proof for expression simplification. *) -Require Import Coq.Program.Equality. -Require Import Axioms. Require Import Coqlib. Require Import Maps. Require Import AST. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 1485dd1..571a937 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -17,13 +17,11 @@ Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. -Require Import Values. Require Import Memory. Require Import AST. Require Import Ctypes. Require Import Cop. Require Import Csyntax. -Require Cstrategy. Require Import Clight. Require Import SimplExpr. diff --git a/common/Behaviors.v b/common/Behaviors.v index 454ea34..0a7ed17 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -18,7 +18,6 @@ Require Import Classical. Require Import ClassicalEpsilon. Require Import Coqlib. -Require Import AST. Require Import Events. Require Import Globalenvs. Require Import Integers. diff --git a/common/Determinism.v b/common/Determinism.v index d798cf5..26a13ab 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -16,7 +16,6 @@ Require Import Coqlib. Require Import AST. Require Import Integers. -Require Import Values. Require Import Events. Require Import Globalenvs. Require Import Smallstep. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 8565ae6..100cab8 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -36,7 +36,6 @@ Require Recdef. Require Import Zwf. -Require Import Axioms. Require Import Coqlib. Require Import Errors. Require Import Maps. diff --git a/common/Smallstep.v b/common/Smallstep.v index 458e8c6..02b18fc 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -22,7 +22,6 @@ Require Import Relations. Require Import Wellfounded. Require Import Coqlib. -Require Import AST. Require Import Events. Require Import Globalenvs. Require Import Integers. diff --git a/driver/Compiler.v b/driver/Compiler.v index 37f7bc2..ed27f38 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -13,12 +13,9 @@ (** The whole compiler and its proof of semantic preservation *) (** Libraries. *) -Require Import Axioms. Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. -Require Import Values. Require Import Smallstep. (** Languages (syntax and semantics). *) Require Csyntax. diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 5a6c1ab..6b7cbf9 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -13,14 +13,10 @@ (** Translation from Mach to IA32 Asm. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index a49a7ff..3d0c57f 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -13,7 +13,6 @@ (** Correctness proof for x86 generation: main proof. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 7ad8a02..0a46677 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -13,7 +13,6 @@ (** Correctness proof for IA32 generation: auxiliary results. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Errors. Require Import Integers. diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v index 1a1ea20..29d2ba0 100644 --- a/ia32/Asmgenretaddr.v +++ b/ia32/Asmgenretaddr.v @@ -17,14 +17,10 @@ return addresses that are stored in activation records. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Errors. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v index cd10698..d4565bd 100644 --- a/ia32/CombineOpproof.v +++ b/ia32/CombineOpproof.v @@ -14,12 +14,10 @@ during the [CSE] phase. *) Require Import Coqlib. -Require Import AST. Require Import Integers. Require Import Values. Require Import Memory. Require Import Op. -Require Import Registers. Require Import RTL. Require Import CombineOp. Require Import CSE. diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index ff5044f..8a612f0 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -17,7 +17,6 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. Require Import Op. Require Import Registers. diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index ca38f6b..1a0508c 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -13,7 +13,6 @@ (** Correctness proof for constant propagation (processor-dependent part). *) Require Import Coqlib. -Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. @@ -29,7 +29,6 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Memdata. Require Import Memory. Require Import Globalenvs. Require Import Events. diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 7bb2bee..0c30386 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -37,14 +37,9 @@ *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Cminor. Require Import Op. Require Import CminorSel. diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index f88f9c0..136a765 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -13,15 +13,12 @@ (** Correctness of instruction selection for operators *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. -Require Import Events. Require Import Globalenvs. -Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 29e65bb..3d5df25 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -21,7 +21,6 @@ Require Export ZArith. Require Export Znumtheory. Require Export List. Require Export Bool. -Require Import Wf_nat. (** * Useful tactics *) diff --git a/lib/Floats.v b/lib/Floats.v index 556cc41..aae2646 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -19,7 +19,6 @@ Require Import Axioms. Require Import Coqlib. Require Import Integers. -Require Import Reals. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. Require Import Fcore. @@ -27,7 +26,6 @@ Require Import Fcalc_round. Require Import Fcalc_bracket. Require Import Fprop_Sterbenz. Require Import Program. -Require Import Omega. Close Scope R_scope. diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 553d905..84d0348 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -15,7 +15,6 @@ (** A persistent union-find data structure. *) -Require Import Wf. Require Recdef. Require Setoid. Require Coq.Program.Wf. diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index b34d939..8ef249d 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -13,14 +13,10 @@ (** Translation from Mach to PPC. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v index 081336c..ddbfda6 100644 --- a/powerpc/Asmgenretaddr.v +++ b/powerpc/Asmgenretaddr.v @@ -17,13 +17,9 @@ return addresses that are stored in activation records. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index c39ccdb..973be92 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -17,7 +17,6 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. Require Import Op. Require Import Registers. diff --git a/powerpc/Op.v b/powerpc/Op.v index 353c51c..e59e15f 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -29,7 +29,6 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Memdata. Require Import Memory. Require Import Globalenvs. Require Import Events. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index fbd2d7b..905a448 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -37,14 +37,9 @@ *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Cminor. Require Import Op. Require Import CminorSel. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 911327c..5e49366 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -19,9 +19,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. -Require Import Events. Require Import Globalenvs. -Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. |