aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-06 19:44:10 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-06 19:44:10 +0000
commit708cd2c7767b497b9ac3dae1ce51973195d00acc (patch)
treeadb042e3603452fc7702db0c6eb55825864e0ded /Makefile
parente231ac08558e959f2ea2664082c62ced9e485c1b (diff)
downloadcompcert-708cd2c7767b497b9ac3dae1ce51973195d00acc.tar.gz
compcert-708cd2c7767b497b9ac3dae1ce51973195d00acc.zip
Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)
Ctyping: relaxation de l'hypothese de typage sur main Cshmgenproof3: adaptation a ces changements. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@82 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions