aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-05-03 14:31:30 +0200
committerCyril SIX <cyril.six@kalray.eu>2019-05-03 14:31:30 +0200
commit9976dba5412be7e834abb63ac2293f1da288a185 (patch)
tree63a6291756643a01bbe75603094334be16eb58eb
parentb6d91977d837c40f243498ae900c5d1abc32f0f2 (diff)
downloadcompcert-kvx-9976dba5412be7e834abb63ac2293f1da288a185.tar.gz
compcert-kvx-9976dba5412be7e834abb63ac2293f1da288a185.zip
Fixing Coq dependencies
-rwxr-xr-xconfigure2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure
index d1880167..fd18d784 100755
--- a/configure
+++ b/configure
@@ -806,7 +806,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\
ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
- Asmblockdeps.v\\
+ Asmblockdeps.v Chunks.v Peephole.v ExtValues.v\\
AbstractBasicBlocksDef.v DepTreeTheory.v ImpDep.v Parallelizability.v\\
ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v
EOF