diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-21 08:17:08 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-21 08:17:08 +0200 |
| commit | d5c95e0799e3b0541b07760178e68a1e72ee1b24 (patch) | |
| tree | 3fe458373a722d5362c1ac2e0c37644598798547 /configure | |
| parent | acc68982e9beb5c26acf336312605c824691f392 (diff) | |
| download | compcert-kvx-d5c95e0799e3b0541b07760178e68a1e72ee1b24.tar.gz compcert-kvx-d5c95e0799e3b0541b07760178e68a1e72ee1b24.zip | |
[WIP: Coq compilation broken] Stub for Asmgen
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -847,8 +847,8 @@ 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\\ ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v\\ - Asmblock.v\\ - Asmgenproof0.v Asmgenproof1.v Asmgenproof.v # TODO: CHANGE THIS + Asmblock.v Asmblockgen.v\\ + Asmgenproof.v # TODO: CHANGE THIS EOF fi |