diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-22 16:03:00 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-22 16:03:00 +0100 |
| commit | 990dae34a6f132b3f7a3be438d47555805831085 (patch) | |
| tree | 3698124d3f5535d1d1578cd53972a1bf55f8b43b /mppa_k1c/PostpassSchedulingproof.v | |
| parent | af3389dbe670eecfaa8ad1a6a2b3ac1454eedfa8 (diff) | |
| download | compcert-kvx-990dae34a6f132b3f7a3be438d47555805831085.tar.gz compcert-kvx-990dae34a6f132b3f7a3be438d47555805831085.zip | |
fix for Coq.8.8 ??
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 57a84480..f5a84db7 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -786,7 +786,6 @@ Proof. Qed. Lemma seqexec_parexec_equiv b ofs f bundle rs rs' m m' o: - (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> @@ -797,7 +796,6 @@ Proof. Qed. Lemma seqexec_parexec_wio b ofs f bundle rs rs' m m': - (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) -> find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> |