diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-29 12:47:56 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-29 12:47:56 +0000 |
| commit | 12421d717405aa7964e437fc1167a23699b61ecc (patch) | |
| tree | 99b975380440ad4e91074f918ee781ec6383f0ce /extraction | |
| parent | dc4bed2cf06f46687225275131f411c86c773598 (diff) | |
Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.
lib/Integers.v: added more properties for ARM port.
lib/Coqlib.v: added more properties for division and powers of 2.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@928 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/.depend | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/extraction/.depend b/extraction/.depend index 4730714..83dc5dc 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -46,6 +46,10 @@ Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi ../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \ Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx +../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \ + ../caml/Camlcoq.cmo CList.cmi AST.cmi +../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \ + ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ CList.cmi AST.cmi ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ @@ -170,7 +174,7 @@ PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \ Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \ - LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi + LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \ Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi Cminor.cmi \ CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi @@ -446,9 +450,11 @@ Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \ Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ Registers.cmi Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \ - LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi + LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi \ + Reload.cmi Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \ - LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi + LTLin.cmx Integers.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx \ + Reload.cmi RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \ Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \ CminorSel.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \ |