diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-08-06 14:47:25 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-08-06 14:47:25 +0000 |
| commit | 538f7ad4feabf9eafe00788ef3a2b65a379d3ee1 (patch) | |
| tree | fa1f727c664f915a89a21a75bf62b467939f1d6b /cfrontend | |
| parent | f91e562a66ebbcac7fab5871ab6189e79653757c (diff) | |
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
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 47bc1c6..6a02e1d 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: |