diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-26 11:52:53 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-26 11:58:21 +0200 |
| commit | 9247603461ccf05167d753e4e023ef5cc692d08d (patch) | |
| tree | e931925d09eec65943033dc52ff82d1a08ad6e05 /mppa_k1c/Asmblockgenproof1.v | |
| parent | 43f1ff52d806099f3bf16726ac2d8a782f4bba98 (diff) | |
| download | compcert-kvx-9247603461ccf05167d753e4e023ef5cc692d08d.tar.gz compcert-kvx-9247603461ccf05167d753e4e023ef5cc692d08d.zip | |
AB: removing bregs
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 8b686676..c996ab1f 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1355,7 +1355,7 @@ Definition noscroll := 0. Ltac bsimpl := unfold exec_bblock; simpl. Lemma Pget_correct: - forall (dst: gpreg) (src: breg) k (rs: regset) m, + forall (dst: gpreg) (src: preg) k (rs: regset) m, src = RA -> exists rs', exec_straight ge fn (Pget dst src ::b k) rs m k rs' m @@ -1365,9 +1365,9 @@ Proof. intros. econstructor; econstructor; econstructor. - rewrite H. bsimpl. auto. - Simpl. -(* - Simpl. +- Simpl. - intros. rewrite H. Simpl. - *)Admitted. +Qed. (* |