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 /lib/Ordered.v | |
parent | e29b0c71f446ea6267711c7cc19294fd93fb81ad (diff) | |
download | compcert-02779dbc71c0f6985427c47ec05dd25b44dd859c.tar.gz compcert-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 'lib/Ordered.v')
-rw-r--r-- | lib/Ordered.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/lib/Ordered.v b/lib/Ordered.v index ce1eca8e..f52a7efd 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -42,7 +42,7 @@ Proof. apply EQ. red. apply Pos.compare_eq_iff. assumption. apply LT. assumption. apply GT. apply Pos.compare_gt_iff. assumption. -Qed. +Defined. Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq. @@ -80,7 +80,7 @@ Proof. assert (Int.unsigned x <> Int.unsigned y). red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence. red. omega. -Qed. +Defined. Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec. @@ -118,14 +118,14 @@ Proof. apply LT. exact l. apply EQ. red; red in e. apply A.index_inj; auto. apply GT. exact l. -Qed. +Defined. Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }. Proof. intros. case (peq (A.index x) (A.index y)); intros. left. apply A.index_inj; auto. right; red; unfold eq; intros; subst. congruence. -Qed. +Defined. End OrderedIndexed. @@ -208,7 +208,7 @@ Proof. apply EQ. red. tauto. apply GT. red. right. split. apply A.eq_sym. auto. auto. apply GT. red. left. auto. -Qed. +Defined. Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }. Proof. @@ -218,7 +218,7 @@ Proof. left; auto. right; intuition. right; intuition. -Qed. +Defined. End OrderedPair. |