diff options
44 files changed, 540 insertions, 364 deletions
@@ -1,172 +1,344 @@ lib/Axioms.vo lib/Axioms.glob lib/Axioms.v.beautified: lib/Axioms.v +lib/Axioms.vio: lib/Axioms.v lib/Coqlib.vo lib/Coqlib.glob lib/Coqlib.v.beautified: lib/Coqlib.v +lib/Coqlib.vio: lib/Coqlib.v lib/Intv.vo lib/Intv.glob lib/Intv.v.beautified: lib/Intv.v lib/Coqlib.vo +lib/Intv.vio: lib/Intv.v lib/Coqlib.vio lib/Maps.vo lib/Maps.glob lib/Maps.v.beautified: lib/Maps.v lib/Coqlib.vo +lib/Maps.vio: lib/Maps.v lib/Coqlib.vio lib/Heaps.vo lib/Heaps.glob lib/Heaps.v.beautified: lib/Heaps.v lib/Coqlib.vo lib/Ordered.vo +lib/Heaps.vio: lib/Heaps.v lib/Coqlib.vio lib/Ordered.vio lib/Lattice.vo lib/Lattice.glob lib/Lattice.v.beautified: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo +lib/Lattice.vio: lib/Lattice.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vo lib/Ordered.glob lib/Ordered.v.beautified: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo +lib/Ordered.vio: lib/Ordered.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Iteration.vo lib/Iteration.glob lib/Iteration.v.beautified: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo lib/Wfsimpl.vo +lib/Iteration.vio: lib/Iteration.v lib/Axioms.vio lib/Coqlib.vio lib/Wfsimpl.vio lib/Integers.vo lib/Integers.glob lib/Integers.v.beautified: lib/Integers.v lib/Coqlib.vo +lib/Integers.vio: lib/Integers.v lib/Coqlib.vio $(ARCH)/Archi.vo $(ARCH)/Archi.glob $(ARCH)/Archi.v.beautified: $(ARCH)/Archi.v flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo +$(ARCH)/Archi.vio: $(ARCH)/Archi.v flocq/Appli/Fappli_IEEE.vio flocq/Appli/Fappli_IEEE_bits.vio lib/Fappli_IEEE_extra.vo lib/Fappli_IEEE_extra.glob lib/Fappli_IEEE_extra.v.beautified: lib/Fappli_IEEE_extra.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Prop/Fprop_Sterbenz.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_rnd_odd.vo +lib/Fappli_IEEE_extra.vio: lib/Fappli_IEEE_extra.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_digits.vio flocq/Calc/Fcalc_ops.vio flocq/Calc/Fcalc_round.vio flocq/Calc/Fcalc_bracket.vio flocq/Prop/Fprop_Sterbenz.vio flocq/Appli/Fappli_IEEE.vio flocq/Appli/Fappli_rnd_odd.vio lib/Floats.vo lib/Floats.glob lib/Floats.v.beautified: lib/Floats.v lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo lib/Fappli_IEEE_extra.vo flocq/Core/Fcore.vo $(ARCH)/Archi.vo +lib/Floats.vio: lib/Floats.v lib/Coqlib.vio lib/Integers.vio flocq/Appli/Fappli_IEEE.vio flocq/Appli/Fappli_IEEE_bits.vio lib/Fappli_IEEE_extra.vio flocq/Core/Fcore.vio $(ARCH)/Archi.vio lib/Parmov.vo lib/Parmov.glob lib/Parmov.v.beautified: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo +lib/Parmov.vio: lib/Parmov.v lib/Axioms.vio lib/Coqlib.vio lib/UnionFind.vo lib/UnionFind.glob lib/UnionFind.v.beautified: lib/UnionFind.v lib/Coqlib.vo +lib/UnionFind.vio: lib/UnionFind.v lib/Coqlib.vio lib/Wfsimpl.vo lib/Wfsimpl.glob lib/Wfsimpl.v.beautified: lib/Wfsimpl.v lib/Axioms.vo +lib/Wfsimpl.vio: lib/Wfsimpl.v lib/Axioms.vio lib/Postorder.vo lib/Postorder.glob lib/Postorder.v.beautified: lib/Postorder.v lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo +lib/Postorder.vio: lib/Postorder.v lib/Coqlib.vio lib/Maps.vio lib/Iteration.vio lib/FSetAVLplus.vo lib/FSetAVLplus.glob lib/FSetAVLplus.v.beautified: lib/FSetAVLplus.v lib/Coqlib.vo +lib/FSetAVLplus.vio: lib/FSetAVLplus.v lib/Coqlib.vio lib/IntvSets.vo lib/IntvSets.glob lib/IntvSets.v.beautified: lib/IntvSets.v lib/Coqlib.vo +lib/IntvSets.vio: lib/IntvSets.v lib/Coqlib.vio lib/Decidableplus.vo lib/Decidableplus.glob lib/Decidableplus.v.beautified: lib/Decidableplus.v lib/Coqlib.vo +lib/Decidableplus.vio: lib/Decidableplus.v lib/Coqlib.vio common/Errors.vo common/Errors.glob common/Errors.v.beautified: common/Errors.v lib/Coqlib.vo +common/Errors.vio: common/Errors.v lib/Coqlib.vio common/AST.vo common/AST.glob common/AST.v.beautified: common/AST.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo +common/AST.vio: common/AST.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Linking.vo common/Linking.glob common/Linking.v.beautified: common/Linking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo +common/Linking.vio: common/Linking.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio common/AST.vio common/Events.vo common/Events.glob common/Events.v.beautified: 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/Events.vio: common/Events.v lib/Coqlib.vio lib/Intv.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Globalenvs.vo common/Globalenvs.glob common/Globalenvs.v.beautified: common/Globalenvs.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo common/Linking.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo +common/Globalenvs.vio: common/Globalenvs.v lib/Axioms.vio lib/Coqlib.vio common/Errors.vio lib/Maps.vio common/AST.vio common/Linking.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Memdata.vo common/Memdata.glob common/Memdata.v.beautified: common/Memdata.v lib/Coqlib.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo +common/Memdata.vio: common/Memdata.v lib/Coqlib.vio $(ARCH)/Archi.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memtype.vo common/Memtype.glob common/Memtype.v.beautified: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo +common/Memtype.vio: common/Memtype.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memdata.vio common/Memory.vo common/Memory.glob common/Memory.v.beautified: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Intv.vo lib/Maps.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo +common/Memory.vio: common/Memory.v lib/Axioms.vio lib/Coqlib.vio lib/Intv.vio lib/Maps.vio $(ARCH)/Archi.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memdata.vio common/Memtype.vio common/Values.vo common/Values.glob common/Values.v.beautified: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo +common/Values.vio: common/Values.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Smallstep.vo common/Smallstep.glob common/Smallstep.v.beautified: common/Smallstep.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo +common/Smallstep.vio: common/Smallstep.v lib/Coqlib.vio common/Events.vio common/Globalenvs.vio lib/Integers.vio common/Behaviors.vo common/Behaviors.glob common/Behaviors.v.beautified: common/Behaviors.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo +common/Behaviors.vio: common/Behaviors.v lib/Coqlib.vio common/Events.vio common/Globalenvs.vio lib/Integers.vio common/Smallstep.vio common/Switch.vo common/Switch.glob common/Switch.v.beautified: common/Switch.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo common/Values.vo +common/Switch.vio: common/Switch.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio common/Values.vio common/Determinism.vo common/Determinism.glob common/Determinism.v.beautified: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo +common/Determinism.vio: common/Determinism.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio common/Behaviors.vio common/Unityping.vo common/Unityping.glob common/Unityping.v.beautified: common/Unityping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo +common/Unityping.vio: common/Unityping.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio common/Separation.vo common/Separation.glob common/Separation.v.beautified: common/Separation.v lib/Coqlib.vo lib/Decidableplus.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo +common/Separation.vio: common/Separation.v lib/Coqlib.vio lib/Decidableplus.vio common/AST.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio backend/Cminor.vo backend/Cminor.glob backend/Cminor.v.beautified: 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 +backend/Cminor.vio: backend/Cminor.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Events.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio common/Switch.vio $(ARCH)/Op.vo $(ARCH)/Op.glob $(ARCH)/Op.v.beautified: $(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 +$(ARCH)/Op.vio: $(ARCH)/Op.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: 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/Smallstep.vo +backend/CminorSel.vio: backend/CminorSel.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Events.vio common/Values.vio common/Memory.vio backend/Cminor.vio $(ARCH)/Op.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)/SelectOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo +$(ARCH)/SelectOp.vio: $(ARCH)/SelectOp.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/CminorSel.vio backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +backend/SelectDiv.vio: backend/SelectDiv.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +backend/SelectLong.vio: backend/SelectLong.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo common/Switch.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo $(ARCH)/Machregs.vo +backend/Selection.vio: backend/Selection.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Errors.vio lib/Integers.vio common/Globalenvs.vio common/Switch.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SelectDiv.vio backend/SelectLong.vio $(ARCH)/Machregs.vio $(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.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.vio: $(ARCH)/SelectOpproof.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.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/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo +backend/SelectDivproof.vio: backend/SelectDivproof.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio $(ARCH)/SelectOpproof.vio backend/SelectDiv.vio backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.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 common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo +backend/SelectLongproof.vio: backend/SelectLongproof.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio $(ARCH)/SelectOpproof.vio backend/SelectLong.vio backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Linking.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo +backend/Selectionproof.vio: backend/Selectionproof.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Linking.vio common/Errors.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio common/Switch.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SelectDiv.vio backend/SelectLong.vio backend/Selection.vio $(ARCH)/SelectOpproof.vio backend/SelectDivproof.vio backend/SelectLongproof.vio backend/Registers.vo backend/Registers.glob backend/Registers.v.beautified: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo common/Values.vo +backend/Registers.vio: backend/Registers.v lib/Coqlib.vio common/AST.vio lib/Maps.vio lib/Ordered.vio common/Values.vio backend/RTL.vo backend/RTL.glob backend/RTL.v.beautified: 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/RTL.vio: backend/RTL.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTLgen.vo backend/RTLgen.glob backend/RTLgen.v.beautified: 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/RTLgen.vio: backend/RTLgen.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Switch.vio $(ARCH)/Op.vio backend/Registers.vio backend/CminorSel.vio backend/RTL.vio backend/RTLgenspec.vo backend/RTLgenspec.glob backend/RTLgenspec.v.beautified: 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/RTLgenspec.vio: backend/RTLgenspec.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Switch.vio $(ARCH)/Op.vio backend/Registers.vio backend/CminorSel.vio backend/RTL.vio backend/RTLgen.vio backend/RTLgenproof.vo backend/RTLgenproof.glob backend/RTLgenproof.v.beautified: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Linking.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/RTLgenproof.vio: backend/RTLgenproof.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Linking.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Smallstep.vio common/Globalenvs.vio common/Switch.vio backend/Registers.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio backend/RTL.vio backend/RTLgen.vio backend/RTLgenspec.vio common/Errors.vio backend/Tailcall.vo backend/Tailcall.glob backend/Tailcall.v.beautified: 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/Tailcall.vio: backend/Tailcall.v lib/Coqlib.vio lib/Maps.vio common/AST.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/Conventions.vio backend/Tailcallproof.vo backend/Tailcallproof.glob backend/Tailcallproof.v.beautified: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo common/AST.vo common/Linking.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/Conventions.vo backend/Tailcall.vo +backend/Tailcallproof.vio: backend/Tailcallproof.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Conventions.vio backend/Tailcall.vio backend/Inlining.vo backend/Inlining.glob backend/Inlining.v.beautified: backend/Inlining.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo +backend/Inlining.vio: backend/Inlining.v lib/Coqlib.vio lib/Wfsimpl.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Inliningspec.vo backend/Inliningspec.glob backend/Inliningspec.v.beautified: backend/Inliningspec.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo +backend/Inliningspec.vio: backend/Inliningspec.v lib/Coqlib.vio lib/Wfsimpl.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Inlining.vio backend/Inliningproof.vo backend/Inliningproof.glob backend/Inliningproof.v.beautified: backend/Inliningproof.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo backend/Inliningspec.vo +backend/Inliningproof.vio: backend/Inliningproof.v lib/Coqlib.vio lib/Wfsimpl.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Inlining.vio backend/Inliningspec.vio backend/Renumber.vo backend/Renumber.glob backend/Renumber.v.beautified: backend/Renumber.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo backend/RTL.vo +backend/Renumber.vio: backend/Renumber.v lib/Coqlib.vio lib/Maps.vio lib/Postorder.vio backend/RTL.vio backend/Renumberproof.vo backend/Renumberproof.glob backend/Renumberproof.v.beautified: backend/Renumberproof.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Renumber.vo +backend/Renumberproof.vio: backend/Renumberproof.v lib/Coqlib.vio lib/Maps.vio lib/Postorder.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Renumber.vio backend/RTLtyping.vo backend/RTLtyping.glob backend/RTLtyping.v.beautified: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo common/Unityping.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Memory.vo common/Events.vo backend/RTL.vo backend/Conventions.vo +backend/RTLtyping.vio: backend/RTLtyping.v lib/Coqlib.vio common/Errors.vio common/Unityping.vio lib/Maps.vio common/AST.vio $(ARCH)/Op.vio backend/Registers.vio common/Globalenvs.vio common/Values.vio lib/Integers.vio common/Memory.vio common/Events.vio backend/RTL.vio backend/Conventions.vio backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo +backend/Kildall.vio: backend/Kildall.v lib/Coqlib.vio lib/Iteration.vio lib/Maps.vio lib/Lattice.vio lib/Heaps.vio backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo +backend/Liveness.vio: backend/Liveness.v lib/Coqlib.vio lib/Maps.vio lib/Lattice.vio common/AST.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Kildall.vio backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified: backend/ValueDomain.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo driver/Compopts.vo common/AST.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Registers.vo backend/RTL.vo +backend/ValueDomain.vio: backend/ValueDomain.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio driver/Compopts.vio common/AST.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Registers.vio backend/RTL.vio $(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)/ValueAOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/ValueDomain.vo backend/RTL.vo +$(ARCH)/ValueAOp.vio: $(ARCH)/ValueAOp.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio $(ARCH)/Op.vio backend/ValueDomain.vio backend/RTL.vio backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo driver/Compopts.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo +backend/ValueAnalysis.vio: backend/ValueAnalysis.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio driver/Compopts.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/Liveness.vio lib/Axioms.vio $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/ValueDomain.vo +$(ARCH)/ConstpropOp.vio: $(ARCH)/ConstpropOp.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/Registers.vio backend/ValueDomain.vio backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo driver/Compopts.vo $(ARCH)/Machregs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo +backend/Constprop.vio: backend/Constprop.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio driver/Compopts.vio $(ARCH)/Machregs.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Liveness.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/ValueAnalysis.vio $(ARCH)/ConstpropOp.vio $(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.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 backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo +$(ARCH)/ConstpropOpproof.vio: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vio driver/Compopts.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/ValueDomain.vio $(ARCH)/ConstpropOp.vio backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo driver/Compopts.vo $(ARCH)/Machregs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOpproof.vo backend/Constprop.vo +backend/Constpropproof.vio: backend/Constpropproof.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio driver/Compopts.vio $(ARCH)/Machregs.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Liveness.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/ValueAnalysis.vio $(ARCH)/ConstpropOp.vio $(ARCH)/ConstpropOpproof.vio backend/Constprop.vio backend/CSEdomain.vo backend/CSEdomain.glob backend/CSEdomain.v.beautified: backend/CSEdomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo +backend/CSEdomain.vio: backend/CSEdomain.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Values.vio common/Memory.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/CSEdomain.vo +$(ARCH)/CombineOp.vio: $(ARCH)/CombineOp.v lib/Coqlib.vio common/AST.vio lib/Integers.vio $(ARCH)/Op.vio backend/CSEdomain.vio backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo +backend/CSE.vio: backend/CSE.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/ValueDomain.vio backend/ValueAnalysis.vio backend/CSEdomain.vio $(ARCH)/CombineOp.vio $(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo +$(ARCH)/CombineOpproof.vio: $(ARCH)/CombineOpproof.v lib/Coqlib.vio lib/Integers.vio common/Values.vio common/Memory.vio $(ARCH)/Op.vio backend/RTL.vio backend/CSEdomain.vio $(ARCH)/CombineOp.vio backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.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/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo +backend/CSEproof.vio: backend/CSEproof.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/ValueAnalysis.vio backend/CSEdomain.vio $(ARCH)/CombineOp.vio $(ARCH)/CombineOpproof.vio backend/CSE.vio backend/NeedDomain.vo backend/NeedDomain.glob backend/NeedDomain.v.beautified: backend/NeedDomain.v lib/Coqlib.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Registers.vo backend/ValueDomain.vo $(ARCH)/Op.vo backend/RTL.vo +backend/NeedDomain.vio: backend/NeedDomain.v lib/Coqlib.vio lib/Maps.vio lib/IntvSets.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio lib/Lattice.vio backend/Registers.vio backend/ValueDomain.vio $(ARCH)/Op.vio backend/RTL.vio $(ARCH)/NeedOp.vo $(ARCH)/NeedOp.glob $(ARCH)/NeedOp.v.beautified: $(ARCH)/NeedOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/NeedDomain.vo backend/RTL.vo +$(ARCH)/NeedOp.vio: $(ARCH)/NeedOp.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio $(ARCH)/Op.vio backend/NeedDomain.vio backend/RTL.vio backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend/Deadcode.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo common/Memory.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo +backend/Deadcode.vio: backend/Deadcode.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Memory.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/ValueDomain.vio backend/ValueAnalysis.vio backend/NeedDomain.vio $(ARCH)/NeedOp.vio backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo +backend/Deadcodeproof.vio: backend/Deadcodeproof.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/ValueDomain.vio backend/ValueAnalysis.vio backend/NeedDomain.vio $(ARCH)/NeedOp.vio backend/Deadcode.vio backend/Unusedglob.vo backend/Unusedglob.glob backend/Unusedglob.v.beautified: backend/Unusedglob.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo lib/Iteration.vo common/Errors.vo common/AST.vo common/Linking.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo +backend/Unusedglob.vio: backend/Unusedglob.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio lib/Iteration.vio common/Errors.vio common/AST.vio common/Linking.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Unusedglobproof.vo backend/Unusedglobproof.glob backend/Unusedglobproof.v.beautified: backend/Unusedglobproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo lib/Iteration.vo common/Errors.vo common/AST.vo common/Linking.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/RTL.vo backend/Unusedglob.vo +backend/Unusedglobproof.vio: backend/Unusedglobproof.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio lib/Iteration.vio common/Errors.vio common/AST.vio common/Linking.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Unusedglob.vio $(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Decidableplus.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo +$(ARCH)/Machregs.vio: $(ARCH)/Machregs.v lib/Coqlib.vio lib/Decidableplus.vio lib/Maps.vio common/AST.vio lib/Integers.vio $(ARCH)/Op.vio backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo +backend/Locations.vio: backend/Locations.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/AST.vio common/Values.vio $(ARCH)/Machregs.vio $(ARCH)/Conventions1.vo $(ARCH)/Conventions1.glob $(ARCH)/Conventions1.v.beautified: $(ARCH)/Conventions1.v lib/Coqlib.vo lib/Decidableplus.vo common/AST.vo common/Events.vo backend/Locations.vo +$(ARCH)/Conventions1.vio: $(ARCH)/Conventions1.v lib/Coqlib.vio lib/Decidableplus.vio common/AST.vio common/Events.vio backend/Locations.vio backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/Conventions1.vo +backend/Conventions.vio: backend/Conventions.v lib/Coqlib.vio common/AST.vio backend/Locations.vio $(ARCH)/Conventions1.vio backend/LTL.vo backend/LTL.glob backend/LTL.v.beautified: 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/LTL.vio: backend/LTL.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Conventions.vio backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo lib/Lattice.vo backend/Kildall.vo common/Memdata.vo $(ARCH)/Archi.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo +backend/Allocation.vio: backend/Allocation.v lib/FSetAVLplus.vio lib/Coqlib.vio lib/Ordered.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio lib/Lattice.vio backend/Kildall.vio common/Memdata.vio $(ARCH)/Archi.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Locations.vio backend/Conventions.vio backend/RTLtyping.vio backend/LTL.vio backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo lib/Lattice.vo backend/Kildall.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Archi.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo backend/Allocation.vo +backend/Allocproof.vio: backend/Allocproof.v lib/Coqlib.vio lib/Ordered.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio lib/Lattice.vio backend/Kildall.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Archi.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Locations.vio backend/Conventions.vio backend/RTLtyping.vio backend/LTL.vio backend/Allocation.vio backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo +backend/Tunneling.vio: backend/Tunneling.v lib/Coqlib.vio lib/Maps.vio lib/UnionFind.vio common/AST.vio backend/LTL.vio backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Linking.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/Tunnelingproof.vio: backend/Tunnelingproof.v lib/Coqlib.vio lib/Maps.vio lib/UnionFind.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Tunneling.vio backend/Linear.vo backend/Linear.glob backend/Linear.v.beautified: 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/Linear.vio: backend/Linear.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Conventions.vio backend/Lineartyping.vo backend/Lineartyping.glob backend/Lineartyping.v.beautified: backend/Lineartyping.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo common/Memory.vo common/Events.vo $(ARCH)/Op.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Linear.vo +backend/Lineartyping.vio: backend/Lineartyping.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Values.vio common/Globalenvs.vio common/Memory.vio common/Events.vio $(ARCH)/Op.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Conventions.vio backend/LTL.vio backend/Linear.vio backend/Linearize.vo backend/Linearize.glob backend/Linearize.v.beautified: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo +backend/Linearize.vio: backend/Linearize.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Linear.vio backend/Linearizeproof.vo backend/Linearizeproof.glob backend/Linearizeproof.v.beautified: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Lattice.vo backend/Kildall.vo lib/Integers.vo common/AST.vo common/Linking.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/Linear.vo backend/Linearize.vo +backend/Linearizeproof.vio: backend/Linearizeproof.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Lattice.vio backend/Kildall.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Linear.vio backend/Linearize.vio backend/CleanupLabels.vo backend/CleanupLabels.glob backend/CleanupLabels.v.beautified: backend/CleanupLabels.v lib/Coqlib.vo lib/Ordered.vo backend/Linear.vo +backend/CleanupLabels.vio: backend/CleanupLabels.v lib/Coqlib.vio lib/Ordered.vio backend/Linear.vio backend/CleanupLabelsproof.vo backend/CleanupLabelsproof.glob backend/CleanupLabelsproof.v.beautified: backend/CleanupLabelsproof.v lib/Coqlib.vo lib/Ordered.vo lib/Integers.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/CleanupLabels.vo +backend/CleanupLabelsproof.vio: backend/CleanupLabelsproof.v lib/Coqlib.vio lib/Ordered.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Linear.vio backend/CleanupLabels.vio backend/Debugvar.vo backend/Debugvar.glob backend/Debugvar.v.beautified: backend/Debugvar.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo +backend/Debugvar.vio: backend/Debugvar.v lib/Axioms.vio lib/Coqlib.vio lib/Maps.vio lib/Iteration.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Conventions.vio backend/Linear.vio backend/Debugvarproof.vo backend/Debugvarproof.glob backend/Debugvarproof.v.beautified: backend/Debugvarproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo $(ARCH)/Op.vo backend/Linear.vo backend/Debugvar.vo +backend/Debugvarproof.vio: backend/Debugvarproof.v lib/Axioms.vio lib/Coqlib.vio lib/Maps.vio lib/Iteration.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Conventions.vio $(ARCH)/Op.vio backend/Linear.vio backend/Debugvar.vio backend/Mach.vo backend/Mach.glob backend/Mach.v.beautified: backend/Mach.v lib/Coqlib.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/Locations.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo +backend/Mach.vio: backend/Mach.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Conventions.vio $(ARCH)/Stacklayout.vio backend/Bounds.vo backend/Bounds.glob backend/Bounds.v.beautified: backend/Bounds.v lib/Coqlib.vo lib/Ordered.vo lib/Intv.vo common/AST.vo $(ARCH)/Op.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo +backend/Bounds.vio: backend/Bounds.v lib/Coqlib.vio lib/Ordered.vio lib/Intv.vio common/AST.vio $(ARCH)/Op.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Linear.vio backend/Conventions.vio $(ARCH)/Stacklayout.vo $(ARCH)/Stacklayout.glob $(ARCH)/Stacklayout.v.beautified: $(ARCH)/Stacklayout.v lib/Coqlib.vo common/Memory.vo common/Separation.vo backend/Bounds.vo +$(ARCH)/Stacklayout.vio: $(ARCH)/Stacklayout.v lib/Coqlib.vio common/Memory.vio common/Separation.vio backend/Bounds.vio backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Lineartyping.vo +backend/Stacking.vio: backend/Stacking.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio common/AST.vio $(ARCH)/Op.vio backend/Locations.vio backend/Linear.vio backend/Mach.vio backend/Bounds.vio backend/Conventions.vio $(ARCH)/Stacklayout.vio backend/Lineartyping.vio backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Separation.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/LTL.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Lineartyping.vo backend/Stacking.vo +backend/Stackingproof.vio: backend/Stackingproof.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Separation.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio backend/LTL.vio $(ARCH)/Op.vio backend/Locations.vio backend/Linear.vio backend/Mach.vio backend/Bounds.vio backend/Conventions.vio $(ARCH)/Stacklayout.vio backend/Lineartyping.vio backend/Stacking.vio $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(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)/Stacklayout.vo backend/Conventions.vo +$(ARCH)/Asm.vio: $(ARCH)/Asm.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio backend/Locations.vio $(ARCH)/Stacklayout.vio backend/Conventions.vio $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo +$(ARCH)/Asmgen.vio: $(ARCH)/Asmgen.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Memdata.vio $(ARCH)/Op.vio backend/Locations.vio backend/Mach.vio $(ARCH)/Asm.vio backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +backend/Asmgenproof0.vio: backend/Asmgenproof0.v lib/Coqlib.vio lib/Intv.vio common/AST.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio backend/Locations.vio backend/Mach.vio $(ARCH)/Asm.vio $(ARCH)/Asmgen.vio backend/Conventions.vio $(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.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 backend/Asmgenproof0.vo backend/Conventions.vo +$(ARCH)/Asmgenproof1.vio: $(ARCH)/Asmgenproof1.v lib/Coqlib.vio common/AST.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio $(ARCH)/Op.vio backend/Locations.vio backend/Mach.vio $(ARCH)/Asm.vio $(ARCH)/Asmgen.vio backend/Asmgenproof0.vio backend/Conventions.vio $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.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/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenproof.vio: $(ARCH)/Asmgenproof.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Mach.vio backend/Conventions.vio $(ARCH)/Asm.vio $(ARCH)/Asmgen.vio backend/Asmgenproof0.vio $(ARCH)/Asmgenproof1.vio cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Linking.vo $(ARCH)/Archi.vo +cfrontend/Ctypes.vio: cfrontend/Ctypes.v lib/Axioms.vio lib/Coqlib.vio lib/Maps.vio common/Errors.vio common/AST.vio common/Linking.vio $(ARCH)/Archi.vio cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: 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/Cop.vio: cfrontend/Cop.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio cfrontend/Ctypes.vio cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Errors.vo common/AST.vo common/Linking.vo common/Values.vo cfrontend/Ctypes.vo cfrontend/Cop.vo +cfrontend/Csyntax.vio: cfrontend/Csyntax.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Errors.vio common/AST.vio common/Linking.vio common/Values.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csem.vo cfrontend/Csem.glob cfrontend/Csem.v.beautified: 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/Csem.vio: cfrontend/Csem.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio common/Smallstep.vio cfrontend/Ctyping.vo cfrontend/Ctyping.glob cfrontend/Ctyping.v.beautified: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Errors.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Ctyping.vio: cfrontend/Ctyping.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Errors.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob cfrontend/Cstrategy.v.beautified: 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/Cstrategy.vio: cfrontend/Cstrategy.v lib/Axioms.vio lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cexec.vo cfrontend/Cexec.glob cfrontend/Cexec.v.beautified: 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/Cexec.vio: cfrontend/Cexec.v lib/Axioms.vio lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Determinism.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio cfrontend/Initializers.vo cfrontend/Initializers.glob cfrontend/Initializers.v.beautified: cfrontend/Initializers.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo +cfrontend/Initializers.vio: cfrontend/Initializers.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Globalenvs.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob cfrontend/Initializersproof.v.beautified: 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/Initializersproof.vio: cfrontend/Initializersproof.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Initializers.vio cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.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/Clight.vo +cfrontend/SimplExpr.vio: cfrontend/SimplExpr.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/AST.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Clight.vio cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.v.beautified: cfrontend/SimplExprspec.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo +cfrontend/SimplExprspec.vio: cfrontend/SimplExprspec.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Memory.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Clight.vio cfrontend/SimplExpr.vio cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob cfrontend/SimplExprproof.v.beautified: cfrontend/SimplExprproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo common/Values.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/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo +cfrontend/SimplExprproof.vio: cfrontend/SimplExprproof.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio cfrontend/Clight.vio cfrontend/SimplExpr.vio cfrontend/SimplExprspec.vio cfrontend/Clight.vo cfrontend/Clight.glob cfrontend/Clight.v.beautified: 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/Clight.vio: cfrontend/Clight.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/ClightBigstep.vo cfrontend/ClightBigstep.glob cfrontend/ClightBigstep.v.beautified: 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/ClightBigstep.vio: cfrontend/ClightBigstep.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio cfrontend/SimplLocals.vo cfrontend/SimplLocals.glob cfrontend/SimplLocals.v.beautified: cfrontend/SimplLocals.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo common/AST.vo common/Linking.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo driver/Compopts.vo +cfrontend/SimplLocals.vio: cfrontend/SimplLocals.v lib/Coqlib.vio lib/Ordered.vio common/Errors.vio common/AST.vio common/Linking.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio driver/Compopts.vio cfrontend/SimplLocalsproof.vo cfrontend/SimplLocalsproof.glob cfrontend/SimplLocalsproof.v.beautified: cfrontend/SimplLocalsproof.v lib/Coqlib.vo common/Errors.vo lib/Ordered.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.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/SimplLocalsproof.vio: cfrontend/SimplLocalsproof.v lib/Coqlib.vio common/Errors.vio lib/Ordered.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio cfrontend/SimplLocals.vio cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob cfrontend/Cshmgen.v.beautified: cfrontend/Cshmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo +cfrontend/Cshmgen.vio: cfrontend/Cshmgen.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio backend/Cminor.vio cfrontend/Csharpminor.vio cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob cfrontend/Cshmgenproof.v.beautified: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.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/Cshmgenproof.vio: cfrontend/Cshmgenproof.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio backend/Cminor.vio cfrontend/Csharpminor.vio cfrontend/Cshmgen.vio cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob cfrontend/Csharpminor.v.beautified: 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 common/Switch.vo backend/Cminor.vo common/Smallstep.vo +cfrontend/Csharpminor.vio: cfrontend/Csharpminor.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Switch.vio backend/Cminor.vio common/Smallstep.vio cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob cfrontend/Cminorgen.v.beautified: cfrontend/Cminorgen.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo cfrontend/Csharpminor.vo backend/Cminor.vo +cfrontend/Cminorgen.vio: cfrontend/Cminorgen.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio cfrontend/Csharpminor.vio backend/Cminor.vio cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob cfrontend/Cminorgenproof.v.beautified: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Intv.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csharpminor.vo common/Switch.vo backend/Cminor.vo cfrontend/Cminorgen.vo +cfrontend/Cminorgenproof.vio: cfrontend/Cminorgenproof.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Intv.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Csharpminor.vio common/Switch.vio backend/Cminor.vio cfrontend/Cminorgen.vio driver/Compopts.vo driver/Compopts.glob driver/Compopts.v.beautified: driver/Compopts.v +driver/Compopts.vio: driver/Compopts.v driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Linking.vo common/Smallstep.vo cfrontend/Ctypes.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/Linear.vo backend/Mach.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/Deadcode.vo backend/Unusedglob.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Debugvar.vo backend/Stacking.vo $(ARCH)/Asmgen.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/Deadcodeproof.vo backend/Unusedglobproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Debugvarproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo driver/Compopts.vo +driver/Compiler.vio: driver/Compiler.v lib/Coqlib.vio common/Errors.vio common/AST.vio common/Linking.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio cfrontend/Cexec.vio cfrontend/Clight.vio cfrontend/Csharpminor.vio backend/Cminor.vio backend/CminorSel.vio backend/RTL.vio backend/LTL.vio backend/Linear.vio backend/Mach.vio $(ARCH)/Asm.vio cfrontend/Initializers.vio cfrontend/SimplExpr.vio cfrontend/SimplLocals.vio cfrontend/Cshmgen.vio cfrontend/Cminorgen.vio backend/Selection.vio backend/RTLgen.vio backend/Tailcall.vio backend/Inlining.vio backend/Renumber.vio backend/Constprop.vio backend/CSE.vio backend/Deadcode.vio backend/Unusedglob.vio backend/Allocation.vio backend/Tunneling.vio backend/Linearize.vio backend/CleanupLabels.vio backend/Debugvar.vio backend/Stacking.vio $(ARCH)/Asmgen.vio cfrontend/SimplExprproof.vio cfrontend/SimplLocalsproof.vio cfrontend/Cshmgenproof.vio cfrontend/Cminorgenproof.vio backend/Selectionproof.vio backend/RTLgenproof.vio backend/Tailcallproof.vio backend/Inliningproof.vio backend/Renumberproof.vio backend/Constpropproof.vio backend/CSEproof.vio backend/Deadcodeproof.vio backend/Unusedglobproof.vio backend/Allocproof.vio backend/Tunnelingproof.vio backend/Linearizeproof.vio backend/CleanupLabelsproof.vio backend/Debugvarproof.vio backend/Stackingproof.vio $(ARCH)/Asmgenproof.vio driver/Compopts.vio driver/Complements.vo driver/Complements.glob driver/Complements.v.beautified: 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 +driver/Complements.vio: driver/Complements.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Values.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio common/Behaviors.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio cfrontend/Clight.vio backend/Cminor.vio backend/RTL.vio $(ARCH)/Asm.vio driver/Compiler.vio common/Errors.vio flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_Raux.glob flocq/Core/Fcore_Raux.v.beautified: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vo +flocq/Core/Fcore_Raux.vio: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vio flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.glob flocq/Core/Fcore_Zaux.v.beautified: flocq/Core/Fcore_Zaux.v +flocq/Core/Fcore_Zaux.vio: flocq/Core/Fcore_Zaux.v flocq/Core/Fcore_defs.vo flocq/Core/Fcore_defs.glob flocq/Core/Fcore_defs.v.beautified: flocq/Core/Fcore_defs.v flocq/Core/Fcore_Raux.vo +flocq/Core/Fcore_defs.vio: flocq/Core/Fcore_defs.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_digits.vo flocq/Core/Fcore_digits.glob flocq/Core/Fcore_digits.v.beautified: flocq/Core/Fcore_digits.v flocq/Core/Fcore_Zaux.vo +flocq/Core/Fcore_digits.vio: flocq/Core/Fcore_digits.v flocq/Core/Fcore_Zaux.vio flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_float_prop.glob flocq/Core/Fcore_float_prop.v.beautified: flocq/Core/Fcore_float_prop.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo +flocq/Core/Fcore_float_prop.vio: flocq/Core/Fcore_float_prop.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FIX.glob flocq/Core/Fcore_FIX.v.beautified: flocq/Core/Fcore_FIX.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_rnd_ne.vo +flocq/Core/Fcore_FIX.vio: flocq/Core/Fcore_FIX.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_rnd_ne.vio flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_FLT.glob flocq/Core/Fcore_FLT.v.beautified: flocq/Core/Fcore_FLT.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_rnd_ne.vo +flocq/Core/Fcore_FLT.vio: flocq/Core/Fcore_FLT.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_rnd_ne.vio flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLX.glob flocq/Core/Fcore_FLX.v.beautified: flocq/Core/Fcore_FLX.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_rnd_ne.vo +flocq/Core/Fcore_FLX.vio: flocq/Core/Fcore_FLX.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_rnd_ne.vio flocq/Core/Fcore_FTZ.vo flocq/Core/Fcore_FTZ.glob flocq/Core/Fcore_FTZ.v.beautified: flocq/Core/Fcore_FTZ.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_FLX.vo +flocq/Core/Fcore_FTZ.vio: flocq/Core/Fcore_FTZ.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_generic_fmt.glob flocq/Core/Fcore_generic_fmt.v.beautified: flocq/Core/Fcore_generic_fmt.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_float_prop.vo +flocq/Core/Fcore_generic_fmt.vio: flocq/Core/Fcore_generic_fmt.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_rnd.glob flocq/Core/Fcore_rnd.v.beautified: flocq/Core/Fcore_rnd.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo +flocq/Core/Fcore_rnd.vio: flocq/Core/Fcore_rnd.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd_ne.vo flocq/Core/Fcore_rnd_ne.glob flocq/Core/Fcore_rnd_ne.v.beautified: flocq/Core/Fcore_rnd_ne.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_ulp.vo +flocq/Core/Fcore_rnd_ne.vio: flocq/Core/Fcore_rnd_ne.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_ulp.glob flocq/Core/Fcore_ulp.v.beautified: flocq/Core/Fcore_ulp.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo +flocq/Core/Fcore_ulp.vio: flocq/Core/Fcore_ulp.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore.vo flocq/Core/Fcore.glob flocq/Core/Fcore.v.beautified: flocq/Core/Fcore.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_rnd_ne.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_ulp.vo +flocq/Core/Fcore.vio: flocq/Core/Fcore.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_rnd_ne.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FLT.vio flocq/Core/Fcore_ulp.vio flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_bracket.glob flocq/Calc/Fcalc_bracket.v.beautified: flocq/Calc/Fcalc_bracket.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo +flocq/Calc/Fcalc_bracket.vio: flocq/Calc/Fcalc_bracket.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_digits.glob flocq/Calc/Fcalc_digits.v.beautified: flocq/Calc/Fcalc_digits.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_digits.vo +flocq/Calc/Fcalc_digits.vio: flocq/Calc/Fcalc_digits.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_div.vo flocq/Calc/Fcalc_div.glob flocq/Calc/Fcalc_div.v.beautified: flocq/Calc/Fcalc_div.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo +flocq/Calc/Fcalc_div.vio: flocq/Calc/Fcalc_div.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_digits.vio flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_ops.glob flocq/Calc/Fcalc_ops.v.beautified: flocq/Calc/Fcalc_ops.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo +flocq/Calc/Fcalc_ops.vio: flocq/Calc/Fcalc_ops.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_round.glob flocq/Calc/Fcalc_round.v.beautified: flocq/Calc/Fcalc_round.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo +flocq/Calc/Fcalc_round.vio: flocq/Calc/Fcalc_round.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_digits.vio flocq/Calc/Fcalc_sqrt.vo flocq/Calc/Fcalc_sqrt.glob flocq/Calc/Fcalc_sqrt.v.beautified: flocq/Calc/Fcalc_sqrt.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_digits.vo flocq/Core/Fcore_float_prop.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo +flocq/Calc/Fcalc_sqrt.vio: flocq/Calc/Fcalc_sqrt.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_digits.vio flocq/Core/Fcore_float_prop.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_digits.vio flocq/Prop/Fprop_div_sqrt_error.vo flocq/Prop/Fprop_div_sqrt_error.glob flocq/Prop/Fprop_div_sqrt_error.v.beautified: flocq/Prop/Fprop_div_sqrt_error.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo flocq/Prop/Fprop_relative.vo +flocq/Prop/Fprop_div_sqrt_error.vio: flocq/Prop/Fprop_div_sqrt_error.v flocq/Core/Fcore.vio flocq/Calc/Fcalc_ops.vio flocq/Prop/Fprop_relative.vio flocq/Prop/Fprop_mult_error.vo flocq/Prop/Fprop_mult_error.glob flocq/Prop/Fprop_mult_error.v.beautified: flocq/Prop/Fprop_mult_error.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo +flocq/Prop/Fprop_mult_error.vio: flocq/Prop/Fprop_mult_error.v flocq/Core/Fcore.vio flocq/Calc/Fcalc_ops.vio flocq/Prop/Fprop_plus_error.vo flocq/Prop/Fprop_plus_error.glob flocq/Prop/Fprop_plus_error.v.beautified: flocq/Prop/Fprop_plus_error.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLT.vo flocq/Calc/Fcalc_ops.vo +flocq/Prop/Fprop_plus_error.vio: flocq/Prop/Fprop_plus_error.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FLT.vio flocq/Calc/Fcalc_ops.vio flocq/Prop/Fprop_relative.vo flocq/Prop/Fprop_relative.glob flocq/Prop/Fprop_relative.v.beautified: flocq/Prop/Fprop_relative.v flocq/Core/Fcore.vo +flocq/Prop/Fprop_relative.vio: flocq/Prop/Fprop_relative.v flocq/Core/Fcore.vio flocq/Prop/Fprop_Sterbenz.vo flocq/Prop/Fprop_Sterbenz.glob flocq/Prop/Fprop_Sterbenz.v.beautified: flocq/Prop/Fprop_Sterbenz.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_generic_fmt.vo flocq/Calc/Fcalc_ops.vo +flocq/Prop/Fprop_Sterbenz.vio: flocq/Prop/Fprop_Sterbenz.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_generic_fmt.vio flocq/Calc/Fcalc_ops.vio flocq/Appli/Fappli_rnd_odd.vo flocq/Appli/Fappli_rnd_odd.glob flocq/Appli/Fappli_rnd_odd.v.beautified: flocq/Appli/Fappli_rnd_odd.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo +flocq/Appli/Fappli_rnd_odd.vio: flocq/Appli/Fappli_rnd_odd.v flocq/Core/Fcore.vio flocq/Calc/Fcalc_ops.vio flocq/Appli/Fappli_double_round.vo flocq/Appli/Fappli_double_round.glob flocq/Appli/Fappli_double_round.v.beautified: flocq/Appli/Fappli_double_round.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_generic_fmt.vo flocq/Calc/Fcalc_ops.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_FTZ.vo +flocq/Appli/Fappli_double_round.vio: flocq/Appli/Fappli_double_round.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_generic_fmt.vio flocq/Calc/Fcalc_ops.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FLT.vio flocq/Core/Fcore_FTZ.vio flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE.glob flocq/Appli/Fappli_IEEE.v.beautified: flocq/Appli/Fappli_IEEE.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_div.vo flocq/Calc/Fcalc_sqrt.vo flocq/Prop/Fprop_relative.vo +flocq/Appli/Fappli_IEEE.vio: flocq/Appli/Fappli_IEEE.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_digits.vio flocq/Calc/Fcalc_round.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_ops.vio flocq/Calc/Fcalc_div.vio flocq/Calc/Fcalc_sqrt.vio flocq/Prop/Fprop_relative.vio flocq/Appli/Fappli_IEEE_bits.vo flocq/Appli/Fappli_IEEE_bits.glob flocq/Appli/Fappli_IEEE_bits.v.beautified: flocq/Appli/Fappli_IEEE_bits.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Appli/Fappli_IEEE.vo +flocq/Appli/Fappli_IEEE_bits.vio: flocq/Appli/Fappli_IEEE_bits.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_digits.vio flocq/Appli/Fappli_IEEE.vio cparser/validator/Alphabet.vo cparser/validator/Alphabet.glob cparser/validator/Alphabet.v.beautified: cparser/validator/Alphabet.v +cparser/validator/Alphabet.vio: cparser/validator/Alphabet.v cparser/validator/Interpreter_complete.vo cparser/validator/Interpreter_complete.glob cparser/validator/Interpreter_complete.v.beautified: cparser/validator/Interpreter_complete.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter.vo cparser/validator/Validator_complete.vo +cparser/validator/Interpreter_complete.vio: cparser/validator/Interpreter_complete.v cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Interpreter.vio cparser/validator/Validator_complete.vio cparser/validator/Interpreter.vo cparser/validator/Interpreter.glob cparser/validator/Interpreter.v.beautified: cparser/validator/Interpreter.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo +cparser/validator/Interpreter.vio: cparser/validator/Interpreter.v cparser/validator/Automaton.vio cparser/validator/Alphabet.vio cparser/validator/Validator_complete.vo cparser/validator/Validator_complete.glob cparser/validator/Validator_complete.v.beautified: cparser/validator/Validator_complete.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo +cparser/validator/Validator_complete.vio: cparser/validator/Validator_complete.v cparser/validator/Automaton.vio cparser/validator/Alphabet.vio cparser/validator/Automaton.vo cparser/validator/Automaton.glob cparser/validator/Automaton.v.beautified: cparser/validator/Automaton.v cparser/validator/Grammar.vo cparser/validator/Alphabet.vo +cparser/validator/Automaton.vio: cparser/validator/Automaton.v cparser/validator/Grammar.vio cparser/validator/Alphabet.vio cparser/validator/Interpreter_correct.vo cparser/validator/Interpreter_correct.glob cparser/validator/Interpreter_correct.v.beautified: cparser/validator/Interpreter_correct.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter.vo +cparser/validator/Interpreter_correct.vio: cparser/validator/Interpreter_correct.v cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Interpreter.vio cparser/validator/Main.vo cparser/validator/Main.glob cparser/validator/Main.v.beautified: cparser/validator/Main.v cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter_safe.vo cparser/validator/Interpreter_correct.vo cparser/validator/Interpreter_complete.vo +cparser/validator/Main.vio: cparser/validator/Main.v cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Interpreter_safe.vio cparser/validator/Interpreter_correct.vio cparser/validator/Interpreter_complete.vio cparser/validator/Validator_safe.vo cparser/validator/Validator_safe.glob cparser/validator/Validator_safe.v.beautified: cparser/validator/Validator_safe.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo +cparser/validator/Validator_safe.vio: cparser/validator/Validator_safe.v cparser/validator/Automaton.vio cparser/validator/Alphabet.vio cparser/validator/Grammar.vo cparser/validator/Grammar.glob cparser/validator/Grammar.v.beautified: cparser/validator/Grammar.v cparser/validator/Alphabet.vo cparser/validator/Tuples.vo +cparser/validator/Grammar.vio: cparser/validator/Grammar.v cparser/validator/Alphabet.vio cparser/validator/Tuples.vio cparser/validator/Interpreter_safe.vo cparser/validator/Interpreter_safe.glob cparser/validator/Interpreter_safe.v.beautified: cparser/validator/Interpreter_safe.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Validator_safe.vo cparser/validator/Interpreter.vo +cparser/validator/Interpreter_safe.vio: cparser/validator/Interpreter_safe.v cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Validator_safe.vio cparser/validator/Interpreter.vio cparser/validator/Tuples.vo cparser/validator/Tuples.glob cparser/validator/Tuples.v.beautified: cparser/validator/Tuples.v +cparser/validator/Tuples.vio: cparser/validator/Tuples.v cparser/Cabs.vo cparser/Cabs.glob cparser/Cabs.v.beautified: cparser/Cabs.v +cparser/Cabs.vio: cparser/Cabs.v cparser/Parser.vo cparser/Parser.glob cparser/Parser.v.beautified: cparser/Parser.v cparser/Cabs.vo cparser/validator/Tuples.vo cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Main.vo +cparser/Parser.vio: cparser/Parser.v cparser/Cabs.vio cparser/validator/Tuples.vio cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Main.vio exportclight/Clightdefs.vo exportclight/Clightdefs.glob exportclight/Clightdefs.v.beautified: exportclight/Clightdefs.v lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo lib/Maps.vo common/Errors.vo +exportclight/Clightdefs.vio: exportclight/Clightdefs.v lib/Integers.vio lib/Floats.vio common/AST.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio lib/Maps.vio common/Errors.vio @@ -8,6 +8,7 @@ *.cmx *.cma *.cmxa +.*.aux *.cmti *.cmt *.merlin @@ -1,3 +1,9 @@ +Release 2.7.1, 2016-07-10 +========================= + +- Ported to Coq 8.5pl2. No other changes in functionality. + + Release 2.7, 2016-06-29 ======================= @@ -21,7 +21,7 @@ DIRS=lib common $(ARCH) backend cfrontend driver debug\ RECDIRS=lib common $(ARCH) backend cfrontend driver flocq exportclight cparser -COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) +COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) COQC="$(COQBIN)coqc" -q $(COQINCLUDES) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) @@ -253,16 +253,13 @@ distclean: check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." -# Problems with coqchk (coq 8.4.pl2): +# Problems with coqchk (coq 8.5pl1): # Integers.Int.Z_mod_modulus_range takes forever to check -# Floats.Float.double_of_bits_of_double takes forever to check -# AST.external_function gives "Failure: impredicative Type inductive type" -# Asm.instruction gives "Failure: impredicative Type inductive type" -# Mach.instruction gives "Failure: impredicative Type inductive type" -# UnionFind.UF.elt gives "Anomaly: Uncaught exception Reduction.NotConvertible" +# compcert.lib.Floats.Float.of_longu_from_words takes forever to check +# compcert.backend.SelectDivproof.divs_mul_shift_2 takes forever to check check-proof: $(FILES) - $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements + $(COQCHK) -admit Integers -admit Floats -admit SelectDivproof Complements print-includes: @echo $(COQINCLUDES) @@ -1,3 +1,3 @@ -version=2.6 +version=2.7.1 buildnr= tag= diff --git a/arm/Archi.v b/arm/Archi.v index e4abf009..6b282022 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -26,7 +26,7 @@ Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). Program Definition default_pl_64 : bool * nan_pl 53 := - (false, nat_iter 51 xO xH). + (false, iter_nat 51 _ xO xH). Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := (** Choose second NaN if pl2 is sNaN but pl1 is qNan. @@ -35,7 +35,7 @@ Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_p negb (Pos.testbit (proj1_sig pl2) 51))%bool. Program Definition default_pl_32 : bool * nan_pl 24 := - (false, nat_iter 22 xO xH). + (false, iter_nat 22 _ xO xH). Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := (** Choose second NaN if pl2 is sNaN but pl1 is qNan. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 7b3f2fdc..90d3b189 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -173,13 +173,13 @@ Definition loadimm (r: ireg) (n: int) (k: code) := let d2 := decompose_int (Int.not n) in let l1 := List.length d1 in let l2 := List.length d2 in - if NPeano.leb l1 1%nat then + if Nat.leb l1 1%nat then Pmov r (SOimm n) :: k - else if NPeano.leb l2 1%nat then + else if Nat.leb l2 1%nat then Pmvn r (SOimm (Int.not n)) :: k else if thumb tt then loadimm_thumb r n k - else if NPeano.leb l1 l2 then + else if Nat.leb l1 l2 then iterate_op (Pmov r) (Porr r r) d1 k else iterate_op (Pmvn r) (Pbic r r) d2 k. @@ -190,7 +190,7 @@ Definition addimm (r1 r2: ireg) (n: int) (k: code) := else (let d1 := decompose_int n in let d2 := decompose_int (Int.neg n) in - if NPeano.leb (List.length d1) (List.length d2) + if Nat.leb (List.length d1) (List.length d2) then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k). @@ -801,4 +801,3 @@ Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := Definition transf_program (p: Mach.program) : res Asm.program := transform_partial_program transf_fundef p. - diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 5bd2b54f..431743c6 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -166,11 +166,11 @@ Proof. intros. unfold loadimm. set (l1 := length (decompose_int n)). set (l2 := length (decompose_int (Int.not n))). - destruct (NPeano.leb l1 1%nat). TailNoLabel. - destruct (NPeano.leb l2 1%nat). TailNoLabel. + destruct (Nat.leb l1 1%nat). TailNoLabel. + destruct (Nat.leb l2 1%nat). TailNoLabel. destruct (thumb tt). unfold loadimm_thumb. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel. - destruct (NPeano.leb l1 l2); auto with labels. + destruct (Nat.leb l1 l2); auto with labels. Qed. Hint Resolve loadimm_label: labels. @@ -179,7 +179,7 @@ Remark addimm_label: Proof. intros; unfold addimm. destruct (Int.ltu (Int.repr (-256)) n). TailNoLabel. - destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); + destruct (Nat.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); auto with labels. Qed. Hint Resolve addimm_label: labels. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 3e222ba4..76a7b080 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -333,11 +333,11 @@ Proof. intros. unfold loadimm. set (l1 := length (decompose_int n)). set (l2 := length (decompose_int (Int.not n))). - destruct (NPeano.leb l1 1%nat). + destruct (Nat.leb l1 1%nat). { (* single mov *) econstructor; split. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } - destruct (NPeano.leb l2 1%nat). + destruct (Nat.leb l2 1%nat). { (* single movn *) econstructor; split. apply exec_straight_one. simpl. rewrite Int.not_involutive. reflexivity. auto. @@ -359,7 +359,7 @@ Proof. rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega. } - destruct (NPeano.leb l1 l2). + destruct (Nat.leb l1 l2). { (* mov - orr* *) replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero). apply iterate_op_correct. @@ -390,7 +390,7 @@ Proof. (* sub *) econstructor; split. apply exec_straight_one; simpl; auto. split; intros; Simpl. apply Val.sub_opp_add. - destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))). + destruct (Nat.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))). (* add - add* *) replace (Val.add (rs r2) (Vint n)) with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)). @@ -1498,5 +1498,3 @@ Proof. Qed. End CONSTRUCTORS. - - diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 26953479..a8d79c3f 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -168,8 +168,7 @@ Proof. + subst b0. apply SETN with (access := fun ofs => Mem.perm m1' b ofs Cur Readable /\ Q b ofs); auto. intros. destruct H5. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - apply H1; auto. -+ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. apply H1; auto. ++ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0). rewrite (Mem.nextblock_storebytes _ _ _ _ _ ST2). eapply ma_nextblock; eauto. @@ -551,7 +550,7 @@ Proof. intros. exploit analyze_successors; eauto. rewrite ANPC; simpl. intros [A B]. econstructor; eauto. eapply eagree_ge; eauto. - eapply magree_monotone; eauto. intros; apply B; auto. + eapply magree_monotone; eauto. Qed. (** Builtin arguments and results *) @@ -1134,5 +1133,3 @@ Proof. Qed. End PRESERVATION. - - diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 23770cb7..f56d6d18 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -512,7 +512,7 @@ Proof. assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. omega. intros. simpl in H. rewrite S1. - transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. + transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; xomega. eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. red; simpl. subst s2; simpl in *. xomega. red; simpl. split. auto. apply align_le. apply min_alignment_pos. @@ -542,7 +542,7 @@ Proof. assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. omega. intros. simpl in H. rewrite S1. - transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. + transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. red; simpl. subst s2; simpl in *; xomega. diff --git a/backend/Kildall.v b/backend/Kildall.v index 87090f5d..a2b49d56 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -74,7 +74,7 @@ Module Type DATAFLOW_SOLVER. point. [transf] is the transfer function, [ep] the entry point, and [ev] the minimal abstract value for [ep]. *) - Variable fixpoint: + Parameter fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t) (ep: positive) (ev: L.t), @@ -83,7 +83,7 @@ Module Type DATAFLOW_SOLVER. (** The [fixpoint_solution] theorem shows that the returned solution, if any, satisfies the dataflow inequations. *) - Hypothesis fixpoint_solution: + Axiom fixpoint_solution: forall A (code: PTree.t A) successors transf ep ev res n instr s, fixpoint code successors transf ep ev = Some res -> code!n = Some instr -> In s (successors instr) -> @@ -93,7 +93,7 @@ Module Type DATAFLOW_SOLVER. (** The [fixpoint_entry] theorem shows that the returned solution, if any, satisfies the additional constraint over the entry point. *) - Hypothesis fixpoint_entry: + Axiom fixpoint_entry: forall A (code: PTree.t A) successors transf ep ev res, fixpoint code successors transf ep ev = Some res -> L.ge res!!ep ev. @@ -102,7 +102,7 @@ Module Type DATAFLOW_SOLVER. and that holds for [L.bot] also holds for the results of the analysis. *) - Hypothesis fixpoint_invariant: + Axiom fixpoint_invariant: forall A (code: PTree.t A) successors transf ep ev (P: L.t -> Prop), P L.bot -> @@ -124,23 +124,23 @@ End DATAFLOW_SOLVER. Module Type NODE_SET. - Variable t: Type. - Variable empty: t. - Variable add: positive -> t -> t. - Variable pick: t -> option (positive * t). - Variable all_nodes: forall {A: Type}, PTree.t A -> t. + Parameter t: Type. + Parameter empty: t. + Parameter add: positive -> t -> t. + Parameter pick: t -> option (positive * t). + Parameter all_nodes: forall {A: Type}, PTree.t A -> t. - Variable In: positive -> t -> Prop. - Hypothesis empty_spec: + Parameter In: positive -> t -> Prop. + Axiom empty_spec: forall n, ~In n empty. - Hypothesis add_spec: + Axiom add_spec: forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. - Hypothesis pick_none: + Axiom pick_none: forall s n, pick s = None -> ~In n s. - Hypothesis pick_some: + Axiom pick_some: forall s n s', pick s = Some(n, s') -> forall n', In n' s <-> n = n' \/ In n' s'. - Hypothesis all_nodes_spec: + Axiom all_nodes_spec: forall A (code: PTree.t A) n instr, code!n = Some instr -> In n (all_nodes code). @@ -900,7 +900,7 @@ Module Type BACKWARD_DATAFLOW_SOLVER. is a finite map returning the list of successors of the given program point. [transf] is the transfer function. *) - Variable fixpoint: + Parameter fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t), option (PMap.t L.t). @@ -908,7 +908,7 @@ Module Type BACKWARD_DATAFLOW_SOLVER. (** The [fixpoint_solution] theorem shows that the returned solution, if any, satisfies the backward dataflow inequations. *) - Hypothesis fixpoint_solution: + Axiom fixpoint_solution: forall A (code: PTree.t A) successors transf res n instr s, fixpoint code successors transf = Some res -> code!n = Some instr -> In s (successors instr) -> @@ -918,12 +918,12 @@ Module Type BACKWARD_DATAFLOW_SOLVER. (** [fixpoint_allnodes] is a variant of [fixpoint], less algorithmically efficient, but correct without any hypothesis on the transfer function. *) - Variable fixpoint_allnodes: + Parameter fixpoint_allnodes: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t), option (PMap.t L.t). - Hypothesis fixpoint_allnodes_solution: + Axiom fixpoint_allnodes_solution: forall A (code: PTree.t A) successors transf res n instr s, fixpoint_allnodes code successors transf = Some res -> code!n = Some instr -> In s (successors instr) -> @@ -1089,11 +1089,11 @@ End Backward_Dataflow_Solver. Module Type ORDERED_TYPE_WITH_TOP. - Variable t: Type. - Variable ge: t -> t -> Prop. - Variable top: t. - Hypothesis top_ge: forall x, ge top x. - Hypothesis refl_ge: forall x, ge x x. + Parameter t: Type. + Parameter ge: t -> t -> Prop. + Parameter top: t. + Axiom top_ge: forall x, ge top x. + Axiom refl_ge: forall x, ge x x. End ORDERED_TYPE_WITH_TOP. @@ -1105,24 +1105,24 @@ Module Type BBLOCK_SOLVER. Declare Module L: ORDERED_TYPE_WITH_TOP. - Variable fixpoint: + Parameter fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t) (entrypoint: positive), option (PMap.t L.t). - Hypothesis fixpoint_solution: + Axiom fixpoint_solution: forall A (code: PTree.t A) successors transf entrypoint res n instr s, fixpoint code successors transf entrypoint = Some res -> code!n = Some instr -> In s (successors instr) -> L.ge res!!s (transf n res!!n). - Hypothesis fixpoint_entry: + Axiom fixpoint_entry: forall A (code: PTree.t A) successors transf entrypoint res, fixpoint code successors transf entrypoint = Some res -> res!!entrypoint = L.top. - Hypothesis fixpoint_invariant: + Axiom fixpoint_invariant: forall A (code: PTree.t A) successors transf entrypoint (P: L.t -> Prop), P L.top -> diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index aad3add4..a57e5ea6 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -865,9 +865,9 @@ Qed. Remark match_call_cont_cont: forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'. Proof. - intros. refine (let cunit : Cminor.program := _ in _). + intros. simple refine (let cunit : Cminor.program := _ in _). econstructor. apply nil. apply nil. apply xH. - refine (let hf : helper_functions := _ in _). + simple refine (let hf : helper_functions := _ in _). econstructor; apply xH. exists cunit, hf; auto. Qed. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index da024a25..0e9c58b3 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1585,7 +1585,7 @@ Lemma find_function_translated: /\ Genv.find_funct_ptr tge bf = Some tf /\ transf_fundef f = OK tf. Proof. - intros until f; intros AG [bound [_ []]] FF. + intros until f; intros AG [bound [_ [?????]]] FF. destruct ros; simpl in FF. - exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF. rewrite Genv.find_funct_find_funct_ptr in FF. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 3c80d733..bc09c3dc 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3739,7 +3739,7 @@ Proof. - (* contents *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r. - set (mv := ZMap.get ofs (Mem.mem_contents m)#b1). + set (mv := ZMap.get ofs (PMap.get b1 (Mem.mem_contents m))). assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)). { Local Transparent Mem.loadbytes. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 2650e0a8..6b2924e4 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -743,7 +743,7 @@ Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econst (* var local *) FinishL. (* var global *) - FinishL. apply red_var_global; auto. + FinishL. (* deref *) Steps H0 (fun x => C(Ederef x ty)). FinishL. (* field struct *) diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 2cd82d8f..48a7a773 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -2291,4 +2291,3 @@ Local Transparent Linker_fundef. type_eq t0 t2 && calling_convention_eq c c0); inv H2. econstructor; split; eauto. Qed. - diff --git a/common/Memory.v b/common/Memory.v index f32d21c7..672012be 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1500,11 +1500,11 @@ Qed. Theorem loadbytes_storebytes_same: loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. Proof. - intros. unfold storebytes in STORE. unfold loadbytes. + intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); try discriminate. rewrite pred_dec_true. - decEq. inv STORE; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat. + decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat. apply getN_setN_same. red; eauto with mem. Qed. diff --git a/common/Separation.v b/common/Separation.v index 6a7ffbea..efcd3281 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -620,7 +620,7 @@ Next Obligation. eauto with mem. } destruct H. constructor. - destruct mi_inj. constructor; intros. -+ eapply Mem.perm_unchanged_on; eauto. eapply IMG; eauto. ++ eapply Mem.perm_unchanged_on; eauto. + eauto. + rewrite (Mem.unchanged_on_contents _ _ _ H0); eauto. - assumption. @@ -630,7 +630,6 @@ Next Obligation. - intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto. eapply mi_perm_inv; eauto. eapply Mem.perm_unchanged_on_2; eauto. - eapply IMG; eauto. Qed. Next Obligation. eapply Mem.valid_block_inject_2; eauto. diff --git a/common/Subtyping.v b/common/Subtyping.v index c09226e0..26b282e0 100644 --- a/common/Subtyping.v +++ b/common/Subtyping.v @@ -30,48 +30,48 @@ Module Type TYPE_ALGEBRA. (** Type expressions *) -Variable t: Type. -Variable eq: forall (x y: t), {x=y} + {x<>y}. -Variable default: t. +Parameter t: Type. +Parameter eq: forall (x y: t), {x=y} + {x<>y}. +Parameter default: t. (** Subtyping *) -Variable sub: t -> t -> Prop. -Hypothesis sub_refl: forall x, sub x x. -Hypothesis sub_trans: forall x y z, sub x y -> sub y z -> sub x z. -Variable sub_dec: forall x y, {sub x y} + {~sub x y}. +Parameter sub: t -> t -> Prop. +Axiom sub_refl: forall x, sub x x. +Axiom sub_trans: forall x y z, sub x y -> sub y z -> sub x z. +Parameter sub_dec: forall x y, {sub x y} + {~sub x y}. (** Least upper bounds. [lub x y] is specified only when [x] and [y] have a common supertype; it can be arbitrary otherwise. *) -Variable lub: t -> t -> t. -Hypothesis lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y). -Hypothesis lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y). -Hypothesis lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z. +Parameter lub: t -> t -> t. +Axiom lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y). +Axiom lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y). +Axiom lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z. (** Greater lower bounds. [glb x y] is specified only when [x] and [y] have a common subtype; it can be arbitrary otherwise.*) -Variable glb: t -> t -> t. -Hypothesis glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x. -Hypothesis glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y. -Hypothesis glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y). +Parameter glb: t -> t -> t. +Axiom glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x. +Axiom glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y. +Axiom glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y). (** Low and high bounds for a given type. *) -Variable low_bound: t -> t. -Variable high_bound: t -> t. -Hypothesis low_bound_sub: forall t, sub (low_bound t) t. -Hypothesis low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x. -Hypothesis high_bound_sub: forall t, sub t (high_bound t). -Hypothesis high_bound_majorant: forall x y, sub x y -> sub y (high_bound x). +Parameter low_bound: t -> t. +Parameter high_bound: t -> t. +Axiom low_bound_sub: forall t, sub (low_bound t) t. +Axiom low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x. +Axiom high_bound_sub: forall t, sub t (high_bound t). +Axiom high_bound_majorant: forall x y, sub x y -> sub y (high_bound x). (** Measure over types *) -Variable weight: t -> nat. -Variable max_weight: nat. -Hypothesis weight_range: forall t, weight t <= max_weight. -Hypothesis weight_sub: forall x y, sub x y -> weight x <= weight y. -Hypothesis weight_sub_strict: forall x y, sub x y -> x <> y -> weight x < weight y. +Parameter weight: t -> nat. +Parameter max_weight: nat. +Axiom weight_range: forall t, weight t <= max_weight. +Axiom weight_sub: forall x y, sub x y -> weight x <= weight y. +Axiom weight_sub_strict: forall x y, sub x y -> x <> y -> weight x < weight y. End TYPE_ALGEBRA. diff --git a/common/Unityping.v b/common/Unityping.v index f9c9d72c..28bcfb5c 100644 --- a/common/Unityping.v +++ b/common/Unityping.v @@ -28,9 +28,9 @@ Local Open Scope error_monad_scope. Module Type TYPE_ALGEBRA. -Variable t: Type. -Variable eq: forall (x y: t), {x=y} + {x<>y}. -Variable default: t. +Parameter t: Type. +Parameter eq: forall (x y: t), {x=y} + {x<>y}. +Parameter default: t. End TYPE_ALGEBRA. @@ -271,15 +271,15 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.4pl*) + 8.5pl2) echo "version $coq_ver -- good!";; ?.*) echo "version $coq_ver -- UNSUPPORTED" - echo "Error: CompCert requires Coq version 8.4, pl1 and up." + echo "Error: CompCert requires Coq version 8.5pl2." missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure Coq version 8.4 pl5 is installed." + echo "Error: make sure Coq version 8.5pl2 is installed." missingtools=true;; esac diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index db850860..2d7f8ff9 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -199,7 +199,7 @@ Next Obligation. apply Zcompare_antisym. Qed. Next Obligation. destruct c. unfold compare31 in *. rewrite Z.compare_eq_iff in *. congruence. -eapply Zcompare_Lt_trans. apply H. apply H0. +eapply Zcompare_Lt_trans. apply H. apply H0. eapply Zcompare_Gt_trans. apply H. apply H0. Qed. Next Obligation. @@ -214,28 +214,27 @@ pose proof (inj_bound_spec x). match goal with |- In x (fst ?p) => destruct p as [] eqn:? end. replace inj_bound with i in H. revert l i Heqp x H. -apply iter_nat_invariant; intros. +induction (Z.abs_nat (phi inj_bound)); intros. inversion Heqp; clear Heqp; subst. -destruct x; specialize (H _ _ (eq_refl _) x0); simpl in *. -rewrite phi_incr in H0. -pose proof (phi_bounded i). -pose proof (phi_bounded (inj x0)). -destruct (Z_lt_le_dec (Zsucc (phi i)) (2 ^ Z_of_nat size)%Z). -rewrite Zmod_small in H0 by omega. -apply Zlt_succ_le, Zle_lt_or_eq in H0. -destruct H0; eauto. -left. -rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; reflexivity. -replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega. -rewrite Z_mod_same_full in H0. +rewrite spec_0 in H. pose proof (phi_bounded (inj x)). omega. +simpl in Heqp. +destruct nat_rect; specialize (IHn _ _ (eq_refl _) x); simpl in *. +inversion Heqp. subst. clear Heqp. +rewrite phi_incr in H. +pose proof (phi_bounded i0). +pose proof (phi_bounded (inj x)). +destruct (Z_lt_le_dec (Zsucc (phi i0)) (2 ^ Z_of_nat size)%Z). +rewrite Zmod_small in H by omega. +apply Zlt_succ_le, Zle_lt_or_eq in H. +destruct H; simpl; auto. left. +rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity. +replace (Zsucc (phi i0)) with (2 ^ Z_of_nat size)%Z in H by omega. +rewrite Z_mod_same_full in H. exfalso; omega. -exfalso; inversion Heqp; subst; - pose proof (phi_bounded (inj x)); change (phi 0) with 0%Z in H; omega. -clear H. rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. pose proof (phi_bounded inj_bound); pose proof (phi_bounded i). rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega. -clear H H0. +clear H H0 H1. do 2 rewrite <- inj_Zabs_nat. f_equal. revert l i Heqp. diff --git a/cparser/validator/Grammar.v b/cparser/validator/Grammar.v index 0768d647..8e427cd9 100644 --- a/cparser/validator/Grammar.v +++ b/cparser/validator/Grammar.v @@ -17,6 +17,7 @@ Require Import List. Require Import Syntax. Require Import Alphabet. Require Import Orders. +Require Tuples. (** The terminal non-terminal alphabets of the grammar. **) Module Type Alphs. @@ -65,7 +66,7 @@ Module Symbol(Import A:Alphs). End Symbol. Module Type T. - Require Export Tuples. + Export Tuples. Include Alphs <+ Symbol. @@ -154,12 +155,12 @@ Module Defs(Import G:T). Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) := match tree with | Terminal_pt _ _ => 1 - | Non_terminal_pt _ _ _ l => S (ptl_size l) + | Non_terminal_pt l => S (ptl_size l) end with ptl_size {head_symbols word sems} (tree:parse_tree_list head_symbols word sems) := match tree with | Nil_ptl => 0 - | Cons_ptl _ _ _ t _ _ _ q => + | Cons_ptl t q => pt_size t + ptl_size q end. End Defs. diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v index 2242065c..a24362f8 100644 --- a/cparser/validator/Interpreter.v +++ b/cparser/validator/Interpreter.v @@ -87,7 +87,7 @@ Variable init : initstate. Definition state_of_stack (stack:stack): state := match stack with | [] => init - | existT s _::_ => s + | existT _ s _::_ => s end. (** [pop] pops some symbols from the stack. It returns the popped semantic @@ -96,15 +96,15 @@ Definition state_of_stack (stack:stack): state := Fixpoint pop (symbols_to_pop:list symbol) (stack_cur:stack): forall {A:Type} (action:arrows_right A (map symbol_semantic_type symbols_to_pop)), result (stack * A) := - match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), _ with + match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), result (stack * A) with | [] => fun A action => OK (stack_cur, action) | t::q => fun A action => match stack_cur with - | existT state_cur sem::stack_rec => + | existT _ state_cur sem::stack_rec => match compare_eqdec (last_symb_of_non_init_state state_cur) t with | left e => let sem_conv := eq_rect _ symbol_semantic_type sem _ e in - pop q stack_rec (action sem_conv) + pop q stack_rec (action sem_conv) | right _ => Err end | [] => Err @@ -147,16 +147,16 @@ Qed. Definition reduce_step stack_cur production buffer: result step_result := do (stack_new, sem) <- pop (prod_rhs_rev production) stack_cur (prod_action' production); - match goto_table (state_of_stack stack_new) (prod_lhs production) return _ with - | Some (exist state_new e) => + match goto_table (state_of_stack stack_new) (prod_lhs production) with + | Some (exist _ state_new e) => let sem := eq_rect _ _ sem _ e in OK (Progress_sr (existT noninitstate_type state_new sem::stack_new) buffer) | None => - match stack_new return _ with + match stack_new with | [] => - match compare_eqdec (prod_lhs production) (start_nt init) return _ with + match compare_eqdec (prod_lhs production) (start_nt init) with | left e => - let sem := eq_rect _ (fun nt => _ (_ nt)) sem _ e in + let sem := eq_rect _ (fun nt => symbol_semantic_type (NT nt)) sem _ e in OK (Accept_sr sem buffer) | right _ => Err end @@ -171,7 +171,7 @@ Definition step stack_cur buffer: result step_result := reduce_step stack_cur production buffer | Lookahead_act awt => match Streams.hd buffer with - | existT term sem => + | existT _ term sem => match awt term with | Shift_act state_new e => let sem_conv := eq_rect _ symbol_semantic_type sem _ e in @@ -213,6 +213,14 @@ Definition parse buffer n_steps: result parse_result := End Init. +Arguments Fail_sr [init]. +Arguments Accept_sr [init] _ _. +Arguments Progress_sr [init] _ _. + +Arguments Fail_pr [init]. +Arguments Timeout_pr [init]. +Arguments Parsed_pr [init] _ _. + End Make. Module Type T(A:Automaton.T). diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index 3d564c11..eb407061 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -147,16 +147,16 @@ with ptl_zipper: Fixpoint ptlz_cost {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems) := match ptlz with - | Non_terminal_pt_ptlz _ _ _ ptz => + | Non_terminal_pt_ptlz ptz => ptz_cost ptz - | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' => + | Cons_ptl_ptlz pt ptlz' => ptlz_cost ptlz' end with ptz_cost {hole_symb hole_word hole_sem} (ptz:pt_zipper hole_symb hole_word hole_sem) := match ptz with | Top_ptz => 0 - | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' => + | Cons_ptl_ptz ptl ptlz' => 1 + ptl_size ptl + ptlz_cost ptlz' end. @@ -172,29 +172,29 @@ Inductive pt_dot: Type := Definition ptd_cost (ptd:pt_dot) := match ptd with | Reduce_ptd ptlz => ptlz_cost ptlz - | Shift_ptd _ _ _ _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz + | Shift_ptd _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz end. Fixpoint ptlz_buffer {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems): Stream token := match ptlz with - | Non_terminal_pt_ptlz _ _ _ ptz => + | Non_terminal_pt_ptlz ptz => ptz_buffer ptz - | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' => + | Cons_ptl_ptlz _ ptlz' => ptlz_buffer ptlz' end with ptz_buffer {hole_symb hole_word hole_sem} (ptz:pt_zipper hole_symb hole_word hole_sem): Stream token := match ptz with | Top_ptz => buffer_end - | Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' => + | @Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' => wordq++ptlz_buffer ptlz' end. Definition ptd_buffer (ptd:pt_dot) := match ptd with | Reduce_ptd ptlz => ptlz_buffer ptlz - | Shift_ptd term sem _ wordq _ _ ptlz => + | @Shift_ptd term sem _ wordq _ _ ptlz => Cons (existT (fun t => symbol_semantic_type (T t)) term sem) (wordq ++ ptlz_buffer ptlz) end. @@ -202,16 +202,16 @@ Definition ptd_buffer (ptd:pt_dot) := Fixpoint ptlz_prod {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems): production := match ptlz with - | Non_terminal_pt_ptlz prod _ _ _ => prod - | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' => + | @Non_terminal_pt_ptlz prod _ _ _ => prod + | Cons_ptl_ptlz _ ptlz' => ptlz_prod ptlz' end. Fixpoint ptlz_past {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems): list symbol := match ptlz with - | Non_terminal_pt_ptlz _ _ _ _ => [] - | Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz' + | Non_terminal_pt_ptlz _ => [] + | @Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz' end. Lemma ptlz_past_ptlz_prod: @@ -236,12 +236,12 @@ Fixpoint ptlz_stack_compat {hole_symbs hole_word hole_sems} (stack:stack): Prop := ptlz_state_compat ptlz (state_of_stack init stack) /\ match ptlz with - | Non_terminal_pt_ptlz _ _ _ ptz => + | Non_terminal_pt_ptlz ptz => ptz_stack_compat ptz stack - | Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' => + | @Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' => match stack with | [] => False - | existT _ sem'::stackq => + | existT _ _ sem'::stackq => ptlz_stack_compat ptlz' stackq /\ sem ~= sem' end @@ -251,7 +251,7 @@ with ptz_stack_compat {hole_symb hole_word hole_sem} (stack:stack): Prop := match ptz with | Top_ptz => stack = [] - | Cons_ptl_ptz _ _ _ _ _ _ _ ptlz' => + | Cons_ptl_ptz _ ptlz' => ptlz_stack_compat ptlz' stack end. @@ -267,7 +267,7 @@ Qed. Definition ptd_stack_compat (ptd:pt_dot) (stack:stack): Prop := match ptd with | Reduce_ptd ptlz => ptlz_stack_compat ptlz stack - | Shift_ptd _ _ _ _ _ _ ptlz => ptlz_stack_compat ptlz stack + | Shift_ptd _ _ _ ptlz => ptlz_stack_compat ptlz stack end. Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} @@ -279,13 +279,13 @@ Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} with | Nil_ptl => fun ptlz => Reduce_ptd ptlz - | Cons_ptl _ _ _ pt _ _ _ ptl' => + | Cons_ptl pt ptl' => match pt in parse_tree hole_symb hole_word hole_sem return ptl_zipper (hole_symb::_) (hole_word++_) (hole_sem,_) -> _ with | Terminal_pt term sem => fun ptlz => Shift_ptd term sem ptl' ptlz - | Non_terminal_pt _ _ _ ptl'' => fun ptlz => + | Non_terminal_pt ptl'' => fun ptlz => build_pt_dot ptl'' (Non_terminal_pt_ptlz (Cons_ptl_ptz ptl' ptlz)) end @@ -360,10 +360,10 @@ Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems} (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } with - | Non_terminal_pt_ptlz prod word sem ptz => fun ptl => + | @Non_terminal_pt_ptlz prod word sem ptz => fun ptl => let sem := uncurry (prod_action prod) sem in existT _ word (existT _ sem (ptz, Non_terminal_pt ptl)) - | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' => fun ptl => + | Cons_ptl_ptlz pt ptlz' => fun ptl => pop_ptlz (Cons_ptl pt ptl) ptlz' end ptl. @@ -371,7 +371,7 @@ Lemma pop_ptlz_cost: forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in ptlz_cost ptlz = ptz_cost ptz. Proof. fix 5. @@ -384,7 +384,7 @@ Lemma pop_ptlz_buffer: forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in ptlz_buffer ptlz = ptz_buffer ptz. Proof. fix 5. @@ -419,7 +419,7 @@ Lemma pop_ptlz_pop_stack_compat: eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _ (pop_ptlz_pop_stack_compat_converter _ _ _ _ _) in - let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with | OK (stack', sem') => ptz_stack_compat ptz stack' /\ sem = sem' @@ -431,7 +431,7 @@ fix 5. destruct ptlz. intros; simpl. split. apply H. -f_equal. +eapply (f_equal (fun X => uncurry X semantic_values)). apply JMeq_eq, JMeq_sym, JMeq_eqrect with (P:=fun x => x). simpl; intros; destruct stack0. destruct (proj2 H). @@ -451,13 +451,13 @@ Qed. Definition next_ptd (ptd:pt_dot): option pt_dot := match ptd with - | Shift_ptd term sem _ _ _ ptl ptlz => + | Shift_ptd term sem ptl ptlz => Some (build_pt_dot ptl (Cons_ptl_ptlz (Terminal_pt term sem) ptlz)) | Reduce_ptd ptlz => - let 'existT _ (existT _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in + let 'existT _ _ (existT _ _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in match ptz in pt_zipper sym _ _ return parse_tree sym _ _ -> _ with | Top_ptz => fun pt => None - | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' => + | Cons_ptl_ptz ptl ptlz' => fun pt => Some (build_pt_dot ptl (Cons_ptl_ptlz pt ptlz')) end pt end. @@ -615,7 +615,7 @@ Definition init_ptd := match head return Type with | T _ => unit | NT _ => pt_dot end with | Terminal_pt _ _ => fun _ => () - | Non_terminal_pt _ _ _ ptl => + | Non_terminal_pt ptl => fun top => build_pt_dot ptl (Non_terminal_pt_ptlz top) end Top_ptz. diff --git a/cparser/validator/Interpreter_correct.v b/cparser/validator/Interpreter_correct.v index 3a285158..1263d4e3 100644 --- a/cparser/validator/Interpreter_correct.v +++ b/cparser/validator/Interpreter_correct.v @@ -59,7 +59,7 @@ Proof. intros. unfold arrows_right, arrows_left. rewrite rev_append_rev, map_app, map_rev, fold_left_app. -f_equal. +apply f_equal. rewrite <- fold_left_rev_right, rev_involutive. reflexivity. Qed. @@ -87,7 +87,7 @@ Lemma pop_invariant: end. Proof. induction symbols_to_pop; intros; unfold pop; fold pop. -exists word_stack ([]:list token) sem_popped; intuition. +exists word_stack, ([]:list token), sem_popped; intuition. f_equal. apply JMeq_eq, JMeq_eqrect with (P:=(fun x => x)). destruct stack_cur as [|[]]; eauto. diff --git a/cparser/validator/Interpreter_safe.v b/cparser/validator/Interpreter_safe.v index f094ddce..a1aa35b8 100644 --- a/cparser/validator/Interpreter_safe.v +++ b/cparser/validator/Interpreter_safe.v @@ -69,15 +69,15 @@ Inductive stack_invariant: stack -> Prop := (symb_stack_of_stack stack) -> prefix_pred (head_states_of_state (state_of_stack init stack)) (state_stack_of_stack stack) -> - stack_invariant_rec stack -> + stack_invariant_next stack -> stack_invariant stack -with stack_invariant_rec: stack -> Prop := - | stack_invariant_rec_nil: - stack_invariant_rec [] - | stack_invariant_rec_cons: +with stack_invariant_next: stack -> Prop := + | stack_invariant_next_nil: + stack_invariant_next [] + | stack_invariant_next_cons: forall state_cur st stack_rec, stack_invariant stack_rec -> - stack_invariant_rec (existT _ state_cur st::stack_rec). + stack_invariant_next (existT _ state_cur st::stack_rec). (** [pop] conserves the stack invariant and does not crash under the assumption that we can pop at this place. diff --git a/cparser/validator/Validator_complete.v b/cparser/validator/Validator_complete.v index 90ab1b0c..a9823278 100644 --- a/cparser/validator/Validator_complete.v +++ b/cparser/validator/Validator_complete.v @@ -276,7 +276,7 @@ Property is_terminal_shift_correct : Proof. unfold is_terminal_shift, terminal_shift. intros. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)). +apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ fut look => _)). intros. destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition. destruct (action_table st); intuition. @@ -327,7 +327,11 @@ Proof. unfold is_end_reduce, end_reduce. intros. revert H1. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)). +apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => _ -> + match action_table st with + | Default_reduce_act p => p = prod + | _ => _ + end)). intros. rewrite H3 in H2. destruct (action_table st); intuition. @@ -368,7 +372,7 @@ Definition non_terminal_goto := match fut with | NT nt::q => match goto_table s1 nt with - | Some (exist s2 _) => + | Some (exist _ s2 _) => state_has_future s2 prod q lookahead | None => forall prod fut lookahead, @@ -386,7 +390,7 @@ Definition is_non_terminal_goto items_map := match future_of_prod prod pos with | NT nt::_ => match goto_table s1 nt with - | Some (exist s2 _) => + | Some (exist _ s2 _) => TerminalSet.subset lset (find_items_map items_map s2 prod (S pos)) | None => forallb_items items_map (fun s1' prod' pos' _ => (implb (compare_eqb s1 s1') @@ -403,7 +407,16 @@ Property is_non_terminal_goto_correct : Proof. unfold is_non_terminal_goto, non_terminal_goto. intros. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)). +apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => + match fut with + | NT nt :: q => + match goto_table st nt with + | Some _ => _ + | None => + forall p f l, state_has_future st p f l -> (_:Prop) + end + | _ => _ + end)). intros. destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition. destruct (goto_table st n) as [[]|]. @@ -414,10 +427,10 @@ rewrite Heql; reflexivity. apply (TerminalSet.subset_2 H2); intuition. intros. remember st in H2; revert Heqs. -apply (forallb_items_spec _ H2 _ _ _ _ H3 (fun _ _ _ _ => _)); intros. -rewrite <- compare_eqb_iff in Heqs; rewrite Heqs in H5. -destruct (future_of_prod prod2 pos0) as [|[]]; intuition. +apply (forallb_items_spec _ H2 _ _ _ _ H3 (fun st' prod fut look => s = st' -> match fut return Prop with [] => _ | _ => _ end)); intros. rewrite <- compare_eqb_iff in H6; rewrite H6 in H5. +destruct (future_of_prod prod1 pos0) as [|[]]; intuition. +rewrite <- compare_eqb_iff in H7; rewrite H7 in H5. discriminate. Qed. @@ -476,7 +489,11 @@ Property is_non_terminal_closed_correct: Proof. unfold is_non_terminal_closed, non_terminal_closed. intros. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)). +apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => + match fut with + | NT nt :: q => forall p l, _ -> _ -> state_has_future st _ _ _ + | _ => _ + end)). intros. destruct (future_of_prod prod0 pos); intuition. destruct s; eauto; intros. diff --git a/cparser/validator/Validator_safe.v b/cparser/validator/Validator_safe.v index c5229ac9..183d661b 100644 --- a/cparser/validator/Validator_safe.v +++ b/cparser/validator/Validator_safe.v @@ -121,7 +121,7 @@ Qed. Definition goto_head_symbs := forall s nt, match goto_table s nt with - | Some (exist s2 _) => + | Some (exist _ s2 _) => prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) | None => True end. @@ -130,7 +130,7 @@ Definition is_goto_head_symbs (_:unit) := forallb (fun s:state => forallb (fun nt => match goto_table s nt with - | Some (exist s2 _) => + | Some (exist _ s2 _) => is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) | None => true end) @@ -235,7 +235,7 @@ Qed. Definition goto_past_state := forall s nt, match goto_table s nt with - | Some (exist s2 _) => + | Some (exist _ s2 _) => prefix_pred (past_state_of_non_init_state s2) (head_states_of_state s) | None => True @@ -245,7 +245,7 @@ Definition is_goto_past_state (_:unit) := forallb (fun s:state => forallb (fun nt => match goto_table s nt with - | Some (exist s2 _) => + | Some (exist _ s2 _) => is_prefix_pred (past_state_of_non_init_state s2) (head_states_of_state s) | None => true diff --git a/extraction/extraction.v b/extraction/extraction.v index 6788bd60..e7f2e2fc 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -166,4 +166,6 @@ Separate Extraction Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg AST.signature_main + Floats.Float32.from_parsed Floats.Float.from_parsed + Globalenvs.Senv.invert_symbol Parser.translation_unit_file. diff --git a/flocq/Calc/Fcalc_round.v b/flocq/Calc/Fcalc_round.v index a1bcb84a..19652d08 100644 --- a/flocq/Calc/Fcalc_round.v +++ b/flocq/Calc/Fcalc_round.v @@ -646,7 +646,7 @@ case Zlt_bool_spec ; intros Hk. (* *) unfold truncate_aux. rewrite Fx at 1. -refine (let H := _ in conj _ H). +unshelve refine (let H := _ in conj _ H). unfold k. ring. rewrite <- H. apply F2R_eq_compat. diff --git a/ia32/Archi.v b/ia32/Archi.v index 267c0eee..ded460d2 100644 --- a/ia32/Archi.v +++ b/ia32/Archi.v @@ -26,13 +26,13 @@ Notation align_int64 := 4%Z (only parsing). Notation align_float64 := 4%Z (only parsing). Program Definition default_pl_64 : bool * nan_pl 53 := - (true, nat_iter 51 xO xH). + (true, iter_nat 51 _ xO xH). Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := false. (**r always choose first NaN *) Program Definition default_pl_32 : bool * nan_pl 24 := - (true, nat_iter 22 xO xH). + (true, iter_nat 22 _ xO xH). Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := false. (**r always choose first NaN *) @@ -43,4 +43,3 @@ Global Opaque big_endian default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. - diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 7e8a1018..5b5d37ee 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -56,8 +56,6 @@ module P = struct let one = Coq_xH let succ = Pos.succ let pred = Pos.pred - let add = Pos.add - let sub = Pos.sub let eq x y = (Pos.compare x y = Eq) let lt x y = (Pos.compare x y = Lt) let gt x y = (Pos.compare x y = Gt) @@ -106,8 +104,6 @@ module P = struct then Coq_xH else Coq_xI (of_int64 (Int64.shift_right_logical n 1)) - let (+) = add - let (-) = sub let (=) = eq let (<) = lt let (<=) = le @@ -124,11 +120,6 @@ module N = struct let zero = N0 let one = Npos Coq_xH - let succ = N.succ - let pred = N.pred - let add = N.add - let sub = N.sub - let mul = N.mul let eq x y = (N.compare x y = Eq) let lt x y = (N.compare x y = Lt) let gt x y = (N.compare x y = Gt) @@ -157,9 +148,6 @@ module N = struct let of_int64 n = if n = 0L then N0 else Npos (P.of_int64 n) - let (+) = add - let (-) = sub - let ( * ) = mul let (=) = eq let (<) = lt let (<=) = le diff --git a/lib/Coqlib.v b/lib/Coqlib.v index fc4a59f6..6fa82492 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -22,6 +22,8 @@ Require Export Znumtheory. Require Export List. Require Export Bool. +Global Set Asymmetric Patterns. + (** * Useful tactics *) Ltac inv H := inversion H; clear H; subst. @@ -768,7 +770,7 @@ Proof. discriminate. rewrite list_length_z_cons. destruct (zeq n 0). generalize (list_length_z_pos l); omega. - exploit IHl; eauto. unfold Zpred. omega. + exploit IHl; eauto. omega. Qed. (** Properties of [List.incl] (list inclusion). *) @@ -1431,4 +1433,3 @@ Lemma nlist_forall2_imply: Proof. induction 1; simpl; intros; constructor; auto. Qed. - diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v index fe7f7c6d..f5ccec2a 100644 --- a/lib/Fappli_IEEE_extra.v +++ b/lib/Fappli_IEEE_extra.v @@ -63,10 +63,10 @@ Qed. Definition is_finite_pos0 (f: binary_float) : bool := match f with - | B754_zero s => negb s - | B754_infinity _ => false - | B754_nan _ _ => false - | B754_finite _ _ _ _ => true + | B754_zero _ _ s => negb s + | B754_infinity _ _ _ => false + | B754_nan _ _ _ _ => false + | B754_finite _ _ _ _ _ _ => true end. Lemma Bsign_pos0: @@ -693,10 +693,10 @@ Qed. Definition ZofB (f: binary_float): option Z := match f with - | B754_finite s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z - | B754_finite s m 0 _ => Some (cond_Zopp s (Zpos m)) - | B754_finite s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z - | B754_zero _ => Some 0%Z + | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z + | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m)) + | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z + | B754_zero _ _ _ => Some 0%Z | _ => None end. @@ -949,7 +949,9 @@ Proof. - revert H H0. fold emin. fold fexp. set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x). set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y). - rewrite (Rmult_comm ry rx). destruct Rlt_bool. + rewrite (Rmult_comm ry rx). + destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode) (rx * ry))) + (bpow radix2 emax)). + intros (A1 & A2 & A3) (B1 & B2 & B3). apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto. rewrite ! Bsign_FF2B. f_equal. f_equal. apply xorb_comm. apply Pos.mul_comm. apply Z.add_comm. @@ -1002,9 +1004,9 @@ Definition Bexact_inverse_mantissa := Z.iter (prec - 1) xO xH. Remark Bexact_inverse_mantissa_value: Zpos Bexact_inverse_mantissa = 2 ^ (prec - 1). Proof. - assert (REC: forall n, Z.pos (nat_iter n xO xH) = 2 ^ (Z.of_nat n)). + assert (REC: forall n, Z.pos (nat_rect _ xH (fun _ => xO) n) = 2 ^ (Z.of_nat n)). { induction n. reflexivity. - simpl nat_iter. transitivity (2 * Z.pos (nat_iter n xO xH)). reflexivity. + simpl nat_rect. transitivity (2 * Z.pos (nat_rect _ xH (fun _ => xO) n)). reflexivity. rewrite inj_S. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega. change (2 ^ 1) with 2. ring. } red in prec_gt_0_. @@ -1015,12 +1017,12 @@ Qed. Remark Bexact_inverse_mantissa_digits2_pos: Z.pos (digits2_pos Bexact_inverse_mantissa) = prec. Proof. - assert (DIGITS: forall n, digits2_pos (nat_iter n xO xH) = Pos.of_nat (n+1)). + assert (DIGITS: forall n, digits2_pos (nat_rect _ xH (fun _ => xO) n) = Pos.of_nat (n+1)). { induction n; simpl. auto. rewrite IHn. destruct n; auto. } red in prec_gt_0_. unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite DIGITS. rewrite Zabs2Nat.abs_nat_nonneg, Z2Nat.inj_sub by omega. - destruct prec; try discriminate. rewrite NPeano.Nat.sub_add. + destruct prec; try discriminate. rewrite Nat.sub_add. simpl. rewrite Pos2Nat.id. auto. simpl. zify; omega. Qed. @@ -1039,7 +1041,7 @@ Qed. Program Definition Bexact_inverse (f: binary_float) : option binary_float := match f with - | B754_finite s m e B => + | B754_finite _ _ s m e B => if positive_eq_dec m Bexact_inverse_mantissa then let e' := -e - (prec - 1) * 2 in if Z_le_dec emin e' then @@ -1125,7 +1127,7 @@ Lemma pos_pow_spec: forall x y, Z.pos (pos_pow x y) = Z.pos x ^ Z.pos y. Proof. intros x. - assert (REC: forall y a, Pos.iter y (Pos.mul x) a = Pos.mul (pos_pow x y) a). + assert (REC: forall y a, Pos.iter (Pos.mul x) a y = Pos.mul (pos_pow x y) a). { induction y; simpl; intros. - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto. - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto. @@ -1347,10 +1349,10 @@ Let binary_float2 := binary_float prec2 emax2. Definition Bconv (conv_nan: bool -> nan_pl prec1 -> bool * nan_pl prec2) (md: mode) (f: binary_float1) : binary_float2 := match f with - | B754_nan s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl - | B754_infinity s => B754_infinity _ _ s - | B754_zero s => B754_zero _ _ s - | B754_finite s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s + | B754_nan _ _ s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl + | B754_infinity _ _ s => B754_infinity _ _ s + | B754_zero _ _ s => B754_zero _ _ s + | B754_finite _ _ s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s end. Theorem Bconv_correct: diff --git a/lib/Floats.v b/lib/Floats.v index cf25852e..51b0c415 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -109,7 +109,7 @@ Module Float. (** Transform a Nan payload to a quiet Nan payload. *) Program Definition transform_quiet_pl (pl:nan_pl 53) : nan_pl 53 := - Pos.lor pl (nat_iter 51 xO xH). + Pos.lor pl (iter_nat xO 51 xH). Next Obligation. destruct pl. simpl. rewrite Z.ltb_lt in *. @@ -147,7 +147,7 @@ Definition expand_pl (pl: nan_pl 24) : nan_pl 53. Proof. refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _). abstract ( - destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_pos; + destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_rect, Fcore_digits.digits2_pos; fold (Fcore_digits.digits2_pos x); rewrite Z.ltb_lt in *; zify; omega). @@ -163,7 +163,7 @@ Definition reduce_pl (pl: nan_pl 53) : nan_pl 24. Proof. refine (exist _ (Pos.shiftr_nat (proj1_sig pl) 29) _). abstract ( - destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_iter; + destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_rect; rewrite Z.ltb_lt in *; assert (forall x, Fcore_digits.digits2_pos (Pos.div2 x) = (Fcore_digits.digits2_pos x - 1)%positive) @@ -473,13 +473,11 @@ Proof. apply Rgt_ge; apply Rcompare_Gt_inv; auto. } assert (EQ: ZofB_range _ _ (sub x y) Int.min_signed Int.max_signed = Some (p - Int.unsigned ox8000_0000)). - { - apply ZofB_range_minus. exact E. + { apply ZofB_range_minus. exact E. compute_this (Int.unsigned ox8000_0000). smart_omega. apply Rge_le; auto. } - unfold to_int; rewrite EQ. simpl. f_equal. unfold Int.sub. f_equal. f_equal. - symmetry; apply Int.unsigned_repr. omega. + unfold to_int; rewrite EQ. simpl. unfold Int.sub. rewrite Int.unsigned_repr by omega. auto. Qed. (** Conversions from ints to floats can be defined as bitwise manipulations @@ -538,7 +536,7 @@ Theorem of_intu_from_words: Proof. intros. pose proof (Int.unsigned_range x). rewrite ! from_words_eq. unfold sub. rewrite BofZ_minus. - unfold of_intu. f_equal. rewrite Int.unsigned_zero. omega. + unfold of_intu. apply (f_equal (BofZ 53 1024 __ __)). rewrite Int.unsigned_zero. omega. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; rewrite Int.unsigned_zero; smart_omega. Qed. @@ -565,7 +563,7 @@ Proof. rewrite ! from_words_eq. rewrite ox8000_0000_signed_unsigned. change (Int.unsigned ox8000_0000) with Int.half_modulus. unfold sub. rewrite BofZ_minus. - unfold of_int. f_equal. omega. + unfold of_int. apply f_equal. omega. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; smart_omega. Qed. @@ -674,7 +672,7 @@ Proof. with ((xh - 2^20) * 2^32) by (compute_this p; compute_this Int.half_modulus; ring). unfold add. rewrite BofZ_plus. - unfold of_long. f_equal. + unfold of_long. apply f_equal. rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add''. fold xh; fold xl. compute_this (two_p 32); ring. apply integer_representable_n2p; auto. @@ -831,7 +829,7 @@ Module Float32. (** ** NaN payload manipulations *) Program Definition transform_quiet_pl (pl:nan_pl 24) : nan_pl 24 := - Pos.lor pl (nat_iter 22 xO xH). + Pos.lor pl (iter_nat xO 22 xH). Next Obligation. destruct pl. simpl. rewrite Z.ltb_lt in *. @@ -1280,4 +1278,3 @@ Global Opaque Float32.to_int Float32.to_intu Float32.to_long Float32.to_longu Float32.add Float32.sub Float32.mul Float32.div Float32.cmp Float32.to_bits Float32.of_bits. - diff --git a/lib/Integers.v b/lib/Integers.v index a0140e57..316dfb52 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -53,7 +53,7 @@ Definition swap_comparison (c: comparison): comparison := (** * Parameterization by the word size, in bits. *) Module Type WORDSIZE. - Variable wordsize: nat. + Parameter wordsize: nat. Axiom wordsize_not_zero: wordsize <> 0%nat. End WORDSIZE. @@ -3378,7 +3378,7 @@ Proof. repeat rewrite unsigned_repr. tauto. generalize wordsize_max_unsigned; omega. generalize wordsize_max_unsigned; omega. - intros. unfold one_bits in H. + unfold one_bits. intros. destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. subst i. apply A. apply Z_one_bits_range with (unsigned x); auto. Qed. @@ -3576,8 +3576,8 @@ Proof. intros. destruct (andb_prop _ _ H1). clear H1. destruct (andb_prop _ _ H2). clear H2. - exploit proj_sumbool_true. eexact H1. intro A; clear H1. - exploit proj_sumbool_true. eexact H4. intro B; clear H4. + apply proj_sumbool_true in H1. + apply proj_sumbool_true in H4. assert (unsigned ofs1 + sz1 <= unsigned ofs2 \/ unsigned ofs2 + sz2 <= unsigned ofs1). destruct (orb_prop _ _ H3). left. eapply proj_sumbool_true; eauto. right. eapply proj_sumbool_true; eauto. clear H3. @@ -248,7 +248,7 @@ Next Obligation. destruct H2. congruence. auto. Qed. Next Obligation. - exists wildcard'0; split; auto. omega. + exists wildcard'; split; auto. omega. Qed. Next Obligation. exists (hi - 1); split; auto. omega. @@ -310,7 +310,3 @@ Hint Resolve disjoint_range in_shift in_shift_inv in_elements elements_in : intv. - - - - diff --git a/lib/Lattice.v b/lib/Lattice.v index 352b4479..4455e22f 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -33,21 +33,21 @@ Local Unset Case Analysis Schemes. Module Type SEMILATTICE. - Variable t: Type. - Variable eq: t -> t -> Prop. - Hypothesis eq_refl: forall x, eq x x. - Hypothesis eq_sym: forall x y, eq x y -> eq y x. - Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Variable beq: t -> t -> bool. - Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. - Variable ge: t -> t -> Prop. - Hypothesis ge_refl: forall x y, eq x y -> ge x y. - Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Variable bot: t. - Hypothesis ge_bot: forall x, ge x bot. - Variable lub: t -> t -> t. - Hypothesis ge_lub_left: forall x y, ge (lub x y) x. - Hypothesis ge_lub_right: forall x y, ge (lub x y) y. + Parameter t: Type. + Parameter eq: t -> t -> Prop. + Axiom eq_refl: forall x, eq x x. + Axiom eq_sym: forall x y, eq x y -> eq y x. + Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Parameter beq: t -> t -> bool. + Axiom beq_correct: forall x y, beq x y = true -> eq x y. + Parameter ge: t -> t -> Prop. + Axiom ge_refl: forall x y, eq x y -> ge x y. + Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Parameter bot: t. + Axiom ge_bot: forall x, ge x bot. + Parameter lub: t -> t -> t. + Axiom ge_lub_left: forall x y, ge (lub x y) x. + Axiom ge_lub_right: forall x y, ge (lub x y) y. End SEMILATTICE. @@ -57,8 +57,8 @@ End SEMILATTICE. Module Type SEMILATTICE_WITH_TOP. Include Type SEMILATTICE. - Variable top: t. - Hypothesis ge_top: forall x, ge top x. + Parameter top: t. + Axiom ge_top: forall x, ge top x. End SEMILATTICE_WITH_TOP. @@ -44,24 +44,24 @@ Set Implicit Arguments. (** * The abstract signatures of trees *) Module Type TREE. - Variable elt: Type. - Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}. - Variable t: Type -> Type. - Variable empty: forall (A: Type), t A. - Variable get: forall (A: Type), elt -> t A -> option A. - Variable set: forall (A: Type), elt -> A -> t A -> t A. - Variable remove: forall (A: Type), elt -> t A -> t A. + Parameter elt: Type. + Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}. + Parameter t: Type -> Type. + Parameter empty: forall (A: Type), t A. + Parameter get: forall (A: Type), elt -> t A -> option A. + Parameter set: forall (A: Type), elt -> A -> t A -> t A. + Parameter remove: forall (A: Type), elt -> t A -> t A. (** The ``good variables'' properties for trees, expressing commutations between [get], [set] and [remove]. *) - Hypothesis gempty: + Axiom gempty: forall (A: Type) (i: elt), get i (empty A) = None. - Hypothesis gss: + Axiom gss: forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x. - Hypothesis gso: + Axiom gso: forall (A: Type) (i j: elt) (x: A) (m: t A), i <> j -> get i (set j x m) = get i m. - Hypothesis gsspec: + Axiom gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A), get i (set j x m) = if elt_eq i j then Some x else get i m. (* We could implement the following, but it's not needed for the moment. @@ -72,18 +72,18 @@ Module Type TREE. forall (A: Type) (i: elt) (m: t A) (v: A), get i m = None -> remove i m = m. *) - Hypothesis grs: + Axiom grs: forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None. - Hypothesis gro: + Axiom gro: forall (A: Type) (i j: elt) (m: t A), i <> j -> get i (remove j m) = get i m. - Hypothesis grspec: + Axiom grspec: forall (A: Type) (i j: elt) (m: t A), get i (remove j m) = if elt_eq i j then None else get i m. (** Extensional equality between trees. *) - Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool. - Hypothesis beq_correct: + Parameter beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool. + Axiom beq_correct: forall (A: Type) (eqA: A -> A -> bool) (t1 t2: t A), beq eqA t1 t2 = true <-> (forall (x: elt), @@ -94,60 +94,60 @@ Module Type TREE. end). (** Applying a function to all data of a tree. *) - Variable map: + Parameter map: forall (A B: Type), (elt -> A -> B) -> t A -> t B. - Hypothesis gmap: + Axiom gmap: forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A), get i (map f m) = option_map (f i) (get i m). (** Same as [map], but the function does not receive the [elt] argument. *) - Variable map1: + Parameter map1: forall (A B: Type), (A -> B) -> t A -> t B. - Hypothesis gmap1: + Axiom gmap1: forall (A B: Type) (f: A -> B) (i: elt) (m: t A), get i (map1 f m) = option_map f (get i m). (** Applying a function pairwise to all data of two trees. *) - Variable combine: + Parameter combine: forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C. - Hypothesis gcombine: + Axiom gcombine: forall (A B C: Type) (f: option A -> option B -> option C), f None None = None -> forall (m1: t A) (m2: t B) (i: elt), get i (combine f m1 m2) = f (get i m1) (get i m2). (** Enumerating the bindings of a tree. *) - Variable elements: + Parameter elements: forall (A: Type), t A -> list (elt * A). - Hypothesis elements_correct: + Axiom elements_correct: forall (A: Type) (m: t A) (i: elt) (v: A), get i m = Some v -> In (i, v) (elements m). - Hypothesis elements_complete: + Axiom elements_complete: forall (A: Type) (m: t A) (i: elt) (v: A), In (i, v) (elements m) -> get i m = Some v. - Hypothesis elements_keys_norepet: + Axiom elements_keys_norepet: forall (A: Type) (m: t A), list_norepet (List.map (@fst elt A) (elements m)). - Hypothesis elements_extensional: + Axiom elements_extensional: forall (A: Type) (m n: t A), (forall i, get i m = get i n) -> elements m = elements n. - Hypothesis elements_remove: + Axiom elements_remove: forall (A: Type) i v (m: t A), get i m = Some v -> exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2. (** Folding a function over all bindings of a tree. *) - Variable fold: + Parameter fold: forall (A B: Type), (B -> elt -> A -> B) -> t A -> B -> B. - Hypothesis fold_spec: + Axiom fold_spec: forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A), fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. (** Same as [fold], but the function does not receive the [elt] argument. *) - Variable fold1: + Parameter fold1: forall (A B: Type), (B -> A -> B) -> t A -> B -> B. - Hypothesis fold1_spec: + Axiom fold1_spec: forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), fold1 f m v = List.fold_left (fun a p => f a (snd p)) (elements m) v. @@ -156,26 +156,26 @@ End TREE. (** * The abstract signatures of maps *) Module Type MAP. - Variable elt: Type. - Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}. - Variable t: Type -> Type. - Variable init: forall (A: Type), A -> t A. - Variable get: forall (A: Type), elt -> t A -> A. - Variable set: forall (A: Type), elt -> A -> t A -> t A. - Hypothesis gi: + Parameter elt: Type. + Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}. + Parameter t: Type -> Type. + Parameter init: forall (A: Type), A -> t A. + Parameter get: forall (A: Type), elt -> t A -> A. + Parameter set: forall (A: Type), elt -> A -> t A -> t A. + Axiom gi: forall (A: Type) (i: elt) (x: A), get i (init x) = x. - Hypothesis gss: + Axiom gss: forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x. - Hypothesis gso: + Axiom gso: forall (A: Type) (i j: elt) (x: A) (m: t A), i <> j -> get i (set j x m) = get i m. - Hypothesis gsspec: + Axiom gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A), get i (set j x m) = if elt_eq i j then x else get i m. - Hypothesis gsident: + Axiom gsident: forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. - Variable map: forall (A B: Type), (A -> B) -> t A -> t B. - Hypothesis gmap: + Parameter map: forall (A B: Type), (A -> B) -> t A -> t B. + Axiom gmap: forall (A B: Type) (f: A -> B) (i: elt) (m: t A), get i (map f m) = f(get i m). End MAP. @@ -1040,10 +1040,10 @@ End PMap. (** * An implementation of maps over any type that injects into type [positive] *) Module Type INDEXED_TYPE. - Variable t: Type. - Variable index: t -> positive. - Hypothesis index_inj: forall (x y: t), index x = index y -> x = y. - Variable eq: forall (x y: t), {x = y} + {x <> y}. + Parameter t: Type. + Parameter index: t -> positive. + Axiom index_inj: forall (x y: t), index x = index y -> x = y. + Parameter eq: forall (x y: t), {x = y} + {x <> y}. End INDEXED_TYPE. Module IMap(X: INDEXED_TYPE). @@ -1148,8 +1148,8 @@ Module NMap := IMap(NIndexed). (** * An implementation of maps over any type with decidable equality *) Module Type EQUALITY_TYPE. - Variable t: Type. - Variable eq: forall (x y: t), {x = y} + {x <> y}. + Parameter t: Type. + Parameter eq: forall (x y: t), {x = y} + {x <> y}. End EQUALITY_TYPE. Module EMap(X: EQUALITY_TYPE) <: MAP. diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 76dd6b31..27278b01 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -26,96 +26,96 @@ Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. Module Type MAP. - Variable elt: Type. - Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}. - Variable t: Type -> Type. - Variable empty: forall (A: Type), t A. - Variable get: forall (A: Type), elt -> t A -> option A. - Variable set: forall (A: Type), elt -> A -> t A -> t A. - Hypothesis gempty: forall (A: Type) (x: elt), get x (empty A) = None. - Hypothesis gsspec: forall (A: Type) (x y: elt) (v: A) (m: t A), + Parameter elt: Type. + Parameter elt_eq: forall (x y: elt), {x=y} + {x<>y}. + Parameter t: Type -> Type. + Parameter empty: forall (A: Type), t A. + Parameter get: forall (A: Type), elt -> t A -> option A. + Parameter set: forall (A: Type), elt -> A -> t A -> t A. + Axiom gempty: forall (A: Type) (x: elt), get x (empty A) = None. + Axiom gsspec: forall (A: Type) (x y: elt) (v: A) (m: t A), get x (set y v m) = if elt_eq x y then Some v else get x m. End MAP. Unset Implicit Arguments. Module Type UNIONFIND. - Variable elt: Type. - Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}. - Variable t: Type. + Parameter elt: Type. + Parameter elt_eq: forall (x y: elt), {x=y} + {x<>y}. + Parameter t: Type. - Variable repr: t -> elt -> elt. - Hypothesis repr_canonical: forall uf a, repr uf (repr uf a) = repr uf a. + Parameter repr: t -> elt -> elt. + Axiom repr_canonical: forall uf a, repr uf (repr uf a) = repr uf a. Definition sameclass (uf: t) (a b: elt) : Prop := repr uf a = repr uf b. - Hypothesis sameclass_refl: + Axiom sameclass_refl: forall uf a, sameclass uf a a. - Hypothesis sameclass_sym: + Axiom sameclass_sym: forall uf a b, sameclass uf a b -> sameclass uf b a. - Hypothesis sameclass_trans: + Axiom sameclass_trans: forall uf a b c, sameclass uf a b -> sameclass uf b c -> sameclass uf a c. - Hypothesis sameclass_repr: + Axiom sameclass_repr: forall uf a, sameclass uf a (repr uf a). - Variable empty: t. - Hypothesis repr_empty: + Parameter empty: t. + Axiom repr_empty: forall a, repr empty a = a. - Hypothesis sameclass_empty: + Axiom sameclass_empty: forall a b, sameclass empty a b -> a = b. - Variable find: t -> elt -> elt * t. - Hypothesis find_repr: + Parameter find: t -> elt -> elt * t. + Axiom find_repr: forall uf a, fst (find uf a) = repr uf a. - Hypothesis find_unchanged: + Axiom find_unchanged: forall uf a x, repr (snd (find uf a)) x = repr uf x. - Hypothesis sameclass_find_1: + Axiom sameclass_find_1: forall uf a x y, sameclass (snd (find uf a)) x y <-> sameclass uf x y. - Hypothesis sameclass_find_2: + Axiom sameclass_find_2: forall uf a, sameclass uf a (fst (find uf a)). - Hypothesis sameclass_find_3: + Axiom sameclass_find_3: forall uf a, sameclass (snd (find uf a)) a (fst (find uf a)). - Variable union: t -> elt -> elt -> t. - Hypothesis repr_union_1: + Parameter union: t -> elt -> elt -> t. + Axiom repr_union_1: forall uf a b x, repr uf x <> repr uf a -> repr (union uf a b) x = repr uf x. - Hypothesis repr_union_2: + Axiom repr_union_2: forall uf a b x, repr uf x = repr uf a -> repr (union uf a b) x = repr uf b. - Hypothesis repr_union_3: + Axiom repr_union_3: forall uf a b, repr (union uf a b) b = repr uf b. - Hypothesis sameclass_union_1: + Axiom sameclass_union_1: forall uf a b, sameclass (union uf a b) a b. - Hypothesis sameclass_union_2: + Axiom sameclass_union_2: forall uf a b x y, sameclass uf x y -> sameclass (union uf a b) x y. - Hypothesis sameclass_union_3: + Axiom sameclass_union_3: forall uf a b x y, sameclass (union uf a b) x y -> sameclass uf x y \/ sameclass uf x a /\ sameclass uf y b \/ sameclass uf x b /\ sameclass uf y a. - Variable merge: t -> elt -> elt -> t. - Hypothesis repr_merge: + Parameter merge: t -> elt -> elt -> t. + Axiom repr_merge: forall uf a b x, repr (merge uf a b) x = repr (union uf a b) x. - Hypothesis sameclass_merge: + Axiom sameclass_merge: forall uf a b x y, sameclass (merge uf a b) x y <-> sameclass (union uf a b) x y. - Variable path_ord: t -> elt -> elt -> Prop. - Hypothesis path_ord_wellfounded: + Parameter path_ord: t -> elt -> elt -> Prop. + Axiom path_ord_wellfounded: forall uf, well_founded (path_ord uf). - Hypothesis path_ord_canonical: + Axiom path_ord_canonical: forall uf x y, repr uf x = x -> ~path_ord uf y x. - Hypothesis path_ord_merge_1: + Axiom path_ord_merge_1: forall uf a b x y, path_ord uf x y -> path_ord (merge uf a b) x y. - Hypothesis path_ord_merge_2: + Axiom path_ord_merge_2: forall uf a b, repr uf a <> repr uf b -> path_ord (merge uf a b) b (repr uf a). - Variable pathlen: t -> elt -> nat. - Hypothesis pathlen_zero: + Parameter pathlen: t -> elt -> nat. + Axiom pathlen_zero: forall uf a, repr uf a = a <-> pathlen uf a = O. - Hypothesis pathlen_merge: + Axiom pathlen_merge: forall uf a b x, pathlen (merge uf a b) x = if elt_eq (repr uf a) (repr uf b) then @@ -124,7 +124,7 @@ Module Type UNIONFIND. pathlen uf x + pathlen uf b + 1 else pathlen uf x. - Hypothesis pathlen_gt_merge: + Axiom pathlen_gt_merge: forall uf a b x y, repr uf x = repr uf y -> pathlen uf x > pathlen uf y -> @@ -652,21 +652,21 @@ Qed. Next Obligation. (* a <> b*) destruct (find_x a') - as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. apply repr_some_diff. auto. Qed. Next Obligation. - destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. rewrite B. apply repr_some. auto. Qed. Next Obligation. split. destruct (find_x a') - as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. symmetry. apply repr_some. auto. intros. rewrite repr_compress. destruct (find_x a') - as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto. + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. auto. Qed. Next Obligation. split; auto. symmetry. apply repr_none. auto. diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v index 4f80822e..a1e4b4ff 100644 --- a/lib/Wfsimpl.v +++ b/lib/Wfsimpl.v @@ -18,7 +18,7 @@ to be defined have non-dependent types, and function extensionality is assumed. *) Require Import Axioms. -Require Import Wf. +Require Import Init.Wf. Require Import Wf_nat. Set Implicit Arguments. @@ -65,4 +65,3 @@ Qed. End FIXM. - diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 8ff11f08..89f53ffd 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -26,13 +26,13 @@ Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). Program Definition default_pl_64 : bool * nan_pl 53 := - (false, nat_iter 51 xO xH). + (false, iter_nat 51 _ xO xH). Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := false. (**r always choose first NaN *) Program Definition default_pl_32 : bool * nan_pl 24 := - (false, nat_iter 22 xO xH). + (false, iter_nat 22 _ xO xH). Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := false. (**r always choose first NaN *) @@ -46,4 +46,3 @@ Global Opaque big_endian (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64: bool. - |