diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-06 17:28:07 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-06 17:28:07 +0200 |
| commit | 5757c5a377b54464b37bdce6a6f9630caefef826 (patch) | |
| tree | 35af24827b363f519a8098366d55a915abec7eb8 /Makefile | |
| parent | c78cfdce8c3af0a923d62ae26a182757204a6031 (diff) | |
| download | compcert-kvx-5757c5a377b54464b37bdce6a6f9630caefef826.tar.gz compcert-kvx-5757c5a377b54464b37bdce6a6f9630caefef826.zip | |
init BTL_SEtheory (by copy/paste from RTLpathSE_theory)
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -143,7 +143,8 @@ SCHEDULING= \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ - BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v + BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ + BTL_SEtheory.v # C front-end modules (in cfrontend/) |