diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-07-25 14:29:28 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-07-25 14:29:28 +0200 |
| commit | 98c22a6f37c7230faf80b6366aaa1c2476f9e67c (patch) | |
| tree | e18195ce1ee65b69c67f05e8dac87d0250cc94c7 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 4ee5d47c502e05deed69eb8ddf183384a86ffd05 (diff) | |
| download | compcert-kvx-98c22a6f37c7230faf80b6366aaa1c2476f9e67c.tar.gz compcert-kvx-98c22a6f37c7230faf80b6366aaa1c2476f9e67c.zip | |
(#139) - Mise à jour du code Coq, oracle
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 5d4fc881..0edaf4e2 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -798,7 +798,7 @@ Lemma verified_schedule_nob_checks_alls_bundles bb lb bundle: List.In bundle lb -> verify_par_bblock bundle = OK tt. Proof. unfold verified_schedule_nob. intros H; - monadInv H. destruct x3. + monadInv H. destruct x4. intros; eapply verified_par_checks_alls_bundles; eauto. Qed. |