diff options
Diffstat (limited to 'ia32/Asmgenproof.v')
| -rw-r--r-- | ia32/Asmgenproof.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index bf14f010..79602e52 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -132,6 +132,13 @@ Proof. Qed. Hint Resolve mk_shrximm_label: labels. +Remark mk_shrxlimm_label: + forall n k c, mk_shrxlimm n k = OK c -> tail_nolabel k c. +Proof. + intros. monadInv H. destruct (Int.eq n Int.zero); TailNoLabel. +Qed. +Hint Resolve mk_shrxlimm_label: labels. + Remark mk_intconv_label: forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> (forall r r', nolabel (f r r')) -> |