From 538f7ad4feabf9eafe00788ef3a2b65a379d3ee1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 6 Aug 2012 14:47:25 +0000 Subject: Remove Val.is_true and Val.is_false, no longer used. Simplified definition of Val.bool_of_val. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 47bc1c63..6a02e1d0 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -443,9 +443,7 @@ Lemma make_boolean_correct: /\ Val.bool_of_val vb b. Proof. assert (VBI: forall n, Val.bool_of_val (Vint n) (negb (Int.eq n Int.zero))). - intros. predSpec Int.eq Int.eq_spec n Int.zero; simpl. - subst. constructor. - constructor. auto. + constructor. intros. functional inversion H0; subst; simpl. exists (Vint n); split; auto. exists (Vint n); split; auto. @@ -458,7 +456,7 @@ Proof. rewrite <- Float.cmp_ne_eq. exists (Val.of_bool (Float.cmp Cne f Float.zero)); split. econstructor; eauto with cshm. - destruct (Float.cmp Cne f Float.zero); simpl; constructor. apply Int.one_not_zero. + destruct (Float.cmp Cne f Float.zero); simpl; constructor. Qed. Lemma make_neg_correct: -- cgit