diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
| commit | 89a54eee40305a61d1c1c0b9c5e6ba039592507b (patch) | |
| tree | 83cf2236e0cc161551cc025af531803547654270 /mppa_k1c/Asmgenproof1.v | |
| parent | 8bdfa912a9ba8cee569cb40bf2ec4c584095e402 (diff) | |
| download | compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.tar.gz compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.zip | |
MPPA - Onegf
Diffstat (limited to 'mppa_k1c/Asmgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 55724239..e5d5af55 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -1534,10 +1534,8 @@ Proof. /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)). { unfold transl_store in TR; destruct chunk; ArgsInv; (econstructor; econstructor; split; [eassumption | split; [ intros; simpl; reflexivity | auto]]). -(* destruct a; auto. apply Mem.store_signed_unsigned_8. destruct a; auto. apply Mem.store_signed_unsigned_16. -*) } destruct A as (mk_instr & chunk' & B & C & D). rewrite D in STORE; clear D. |