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 --- lib/Ordered.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'lib/Ordered.v') 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. -- cgit