aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-30 18:46:50 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-30 18:46:50 +0200
commit27c8e10f4e0a3eee6bf9feb03d0f12990f74badd (patch)
tree7761f2d1e53a8d4bd0c47d0b40411c46c1bfe3ad /Makefile
parentb937a4c10226930b7109ae6c9707255e53a0dd2b (diff)
downloadcompcert-kvx-27c8e10f4e0a3eee6bf9feb03d0f12990f74badd.tar.gz
compcert-kvx-27c8e10f4e0a3eee6bf9feb03d0f12990f74badd.zip
use inject_l
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 4cf9ccf1..f005d048 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,7 @@ BACKEND=\
Kildall.v Liveness.v \
ValueDomain.v ValueAOp.v ValueAnalysis.v \
ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
- Inject.v \
+ Inject.v Injectproof.v \
CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
CSE2deps.v CSE2depsproof.v \
CSE2.v CSE2proof.v \