aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-08-29 14:48:55 +0200
committerCyril SIX <cyril.six@kalray.eu>2018-09-06 15:58:31 +0200
commite2c15a3957cfcbab1ff0aaf30a8450c3e177a30a (patch)
treeeba0e185ab01f2215bccac4e156134097a436e7f /Makefile
parent96de003cd1b9e486781263a48ca10da047937c80 (diff)
downloadcompcert-kvx-e2c15a3957cfcbab1ff0aaf30a8450c3e177a30a.tar.gz
compcert-kvx-e2c15a3957cfcbab1ff0aaf30a8450c3e177a30a.zip
Asmblockgen.v finished (no proof yet)
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index a9cda92c..9a9245d2 100644
--- a/Makefile
+++ b/Makefile
@@ -96,7 +96,7 @@ BACKEND=\
Mach.v \
Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
Machblock.v Machblockgen.v Machblockgenproof.v \
- Asmblock.v \
+ Asmblock.v Asmblockgen.v \
Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v
# C front-end modules (in cfrontend/)