summaryrefslogtreecommitdiff
path: root/cfrontend/Cshmgenproof.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-08-06 14:47:25 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-08-06 14:47:25 +0000
commit538f7ad4feabf9eafe00788ef3a2b65a379d3ee1 (patch)
treefa1f727c664f915a89a21a75bf62b467939f1d6b /cfrontend/Cshmgenproof.v
parentf91e562a66ebbcac7fab5871ab6189e79653757c (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/Cshmgenproof.v')
-rw-r--r--cfrontend/Cshmgenproof.v6
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: