diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 10:50:14 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 10:50:14 +0100 |
| commit | 20745c6ce58093bca0b1c8d696444ed9be5f47a9 (patch) | |
| tree | 9252fd03b5cfa265cebdd8f983822e0e95f79593 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | b66c1d482292c15e3d7907262cf1c94edabdd40e (diff) | |
| download | compcert-kvx-20745c6ce58093bca0b1c8d696444ed9be5f47a9.tar.gz compcert-kvx-20745c6ce58093bca0b1c8d696444ed9be5f47a9.zip | |
Proving the axiom verified_schedule_single_inst
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 64489e16..16965af4 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -56,8 +56,6 @@ Axiom verified_schedule_correct: concat_all lbb = OK tbb
/\ bblock_equiv ge f bb tbb.
-Axiom verified_schedule_single_inst: forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).
-
Axiom verified_schedule_header:
forall bb tbb lbb,
verified_schedule bb = OK (tbb :: lbb) ->
|