diff options
Diffstat (limited to 'backend/ValueDomain.v')
| -rw-r--r-- | backend/ValueDomain.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 8b76f44d..3c80d733 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3766,6 +3766,9 @@ Proof. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r. split. omega. apply Int.unsigned_range_2. +- (* perm inv *) + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + rewrite Zplus_0_r in H2. auto. Qed. Lemma inj_of_bc_preserves_globals: |