From 02779dbc71c0f6985427c47ec05dd25b44dd859c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 10 Mar 2013 12:13:12 +0000 Subject: 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 --- cfrontend/Initializersproof.v | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'cfrontend/Initializersproof.v') 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: -- cgit