From ce0892a2a279c2cf5777b630810749dcc85b6a6e Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 5 May 2010 13:42:31 +0000 Subject: Strengthen chunktype inference and use it to remove some useless casts. Finished proof of chunktype_compat, which was incomplete. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1335 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to '.depend') diff --git a/.depend b/.depend index bf0028f..4308398 100644 --- a/.depend +++ b/.depend @@ -20,7 +20,7 @@ common/Smallstep.vo: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Event common/Determinism.vo: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo -$(ARCH)/Op.vo: $(ARCH)/Op.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: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo backend/CminorSel.vo: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo $(ARCH)/SelectOp.vo: $(ARCH)/SelectOp.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/Selection.vo: backend/Selection.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo -- cgit v1.2.3