diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 08:12:37 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 08:12:37 +0200 |
| commit | 5dec4b189dd7775229199de11e4c81551b7baaf6 (patch) | |
| tree | 6ef4f77034cd9003256e34e31e5b91c35a4e1b85 /configure | |
| parent | 0cde06d359ff8b265b38eef5f62a2e8f4e744059 (diff) | |
| download | compcert-kvx-5dec4b189dd7775229199de11e4c81551b7baaf6.tar.gz compcert-kvx-5dec4b189dd7775229199de11e4c81551b7baaf6.zip | |
restauring Coq compilation with STUBS
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 5 |
1 files changed, 2 insertions, 3 deletions
@@ -845,10 +845,9 @@ if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling cat >> Makefile.config <<EOF ARCHDIRS=$arch kvx/lib kvx/abstractbb kvx/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v ForwardSimulationBlock.v\\ - AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ + AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v\\ ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v\\ - Asmblock.v Asmblockgen.v\\ - Asmgenproof.v # TODO: CHANGE THIS + Asmblock.v Asmblockgen.v Asmblockgenproof.v # TODO: UPDATE THIS EOF fi |