diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-02 07:48:50 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-02 07:48:50 +0200 |
| commit | 9f440451e0694eddf66318bf2cde9bf25c32ab83 (patch) | |
| tree | 0349aec40b2221fde00746b2aeeebf8a16527af1 /configure | |
| parent | 5e116ac1b0254e7904a543d357009c0125ecf423 (diff) | |
| download | compcert-kvx-9f440451e0694eddf66318bf2cde9bf25c32ab83.tar.gz compcert-kvx-9f440451e0694eddf66318bf2cde9bf25c32ab83.zip | |
remove useless (and unprovable) lemmas on completeness of the refinement
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -845,7 +845,7 @@ EXECUTE=kvx-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __KVX_COS__ SIMU=kvx-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ + RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ |