From 6f3225b0623b9c97eed7d40ddc320b08c79c6518 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 10 Feb 2013 10:08:27 +0000 Subject: 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 --- lib/Ordered.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'lib/Ordered.v') 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. -- cgit