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 | |
| parent | af3389dbe670eecfaa8ad1a6a2b3ac1454eedfa8 (diff) | |
| download | compcert-kvx-990dae34a6f132b3f7a3be438d47555805831085.tar.gz compcert-kvx-990dae34a6f132b3f7a3be438d47555805831085.zip | |
fix for Coq.8.8 ??
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 5 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 0c6c74fb..35138123 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1463,7 +1463,8 @@ Definition bblock_para_check (p: Asmblock.bblock) : bool := Require Import Asmvliw. Import PChk. -Section SECT. +Section SECT_PAR. + Variable Ge: genv. Theorem forward_simu_par: @@ -1526,4 +1527,4 @@ Proof. + clear MO. unfold exec in EXEC. rewrite EXEC in PRUN. discriminate. Qed. -End SECT. +End SECT_PAR. 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' -> |