diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-10 10:08:27 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-10 10:08:27 +0000 |
| commit | 6f3225b0623b9c97eed7d40ddc320b08c79c6518 (patch) | |
| tree | be4ea0d5624499c40f82d3c2f86c0fba7ead6aef /lib/Ordered.v | |
| parent | 77d3c45aa0928420a083a8d25ec52d5f7f3e6c77 (diff) | |
| download | compcert-kvx-6f3225b0623b9c97eed7d40ddc320b08c79c6518.tar.gz compcert-kvx-6f3225b0623b9c97eed7d40ddc320b08c79c6518.zip | |
lib/Integers.v: revised and extended, faster implementation based on
bit-level operations provided by ZArith in Coq 8.4.
Other modules: adapted accordingly.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Ordered.v')
| -rw-r--r-- | lib/Ordered.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/lib/Ordered.v b/lib/Ordered.v index 1c7c7f43..ce1eca8e 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -38,12 +38,10 @@ Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof Plt_ne. Lemma compare : forall x y : t, Compare lt eq x y. Proof. - intros. case (plt x y); intro. - apply LT. auto. - case (peq x y); intro. - apply EQ. auto. - apply GT. red; unfold Plt in *. - assert (Zpos x <> Zpos y). congruence. omega. + intros. destruct (Pos.compare x y) as [] eqn:E. + apply EQ. red. apply Pos.compare_eq_iff. assumption. + apply LT. assumption. + apply GT. apply Pos.compare_gt_iff. assumption. Qed. Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq. |