diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-10 12:13:12 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-10 12:13:12 +0000 |
| commit | 02779dbc71c0f6985427c47ec05dd25b44dd859c (patch) | |
| tree | cdff116e8c7e5d82ae6943428018f39d1ce81d60 /cfrontend/Initializersproof.v | |
| parent | e29b0c71f446ea6267711c7cc19294fd93fb81ad (diff) | |
| download | compcert-kvx-02779dbc71c0f6985427c47ec05dd25b44dd859c.tar.gz compcert-kvx-02779dbc71c0f6985427c47ec05dd25b44dd859c.zip | |
Glasnost: making transparent a number of definitions that were opaque
for no good reason.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Initializersproof.v')
| -rw-r--r-- | cfrontend/Initializersproof.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index b64c3097..b0884ac1 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -397,13 +397,11 @@ Proof. Opaque zeq. intros. unfold sem_cmp in *. destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval. - destruct (Int.eq n Int.zero); try discriminate. +- destruct (Int.eq n Int.zero); try discriminate. unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor. - destruct (Int.eq n Int.zero); try discriminate. +- destruct (Int.eq n Int.zero); try discriminate. unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor. - rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. - rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4. - destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. +- destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. Qed. Lemma sem_binary_match: |