diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-09-12 11:13:30 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-09-12 11:13:30 +0200 |
| commit | de208f6e67fb5fbc94ecd9f9e98804bcdeb14fa5 (patch) | |
| tree | c158c82a4a1a8f63a275bb2e6346d4ccce33d9ba /configure | |
| parent | 270de4756f01a4883c896292446648983601326f (diff) | |
| download | compcert-kvx-de208f6e67fb5fbc94ecd9f9e98804bcdeb14fa5.tar.gz compcert-kvx-de208f6e67fb5fbc94ecd9f9e98804bcdeb14fa5.zip | |
RTLpath: simplifying (a bit) the proof
by simplifying a bit a pedantic condition
on wellformed path.
Diffstat (limited to 'configure')
0 files changed, 0 insertions, 0 deletions