aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-08-29 16:50:23 +0200
committerCyril SIX <cyril.six@kalray.eu>2018-09-06 15:58:31 +0200
commit63737a502b0f0b6c1369641e9d3d9f05712e74f7 (patch)
tree920304519a0d4d20a519d4a810e9a3c2aae7ee05 /Makefile
parente2c15a3957cfcbab1ff0aaf30a8450c3e177a30a (diff)
downloadcompcert-kvx-63737a502b0f0b6c1369641e9d3d9f05712e74f7.tar.gz
compcert-kvx-63737a502b0f0b6c1369641e9d3d9f05712e74f7.zip
Asmblock: Adding forward_simulation and determinism as axioms
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 9a9245d2..e0dd86e2 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 Asmblockgen.v \
+ Asmblock.v Asmblockgen.v Asmblockgenproof.v \
Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v
# C front-end modules (in cfrontend/)