From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 20 Apr 2013 07:54:52 +0000
Subject: Big merge of the newregalloc-int64 branch.  Lots of changes in two
 directions: 1- new register allocator (+ live range splitting,
 spilling&reloading, etc)    based on a posteriori validation using the
 Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long
 long").

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index b936b9b2..ce5d94eb 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -559,6 +559,16 @@ Proof.
 Defined.
 Global Opaque Zdivide_dec.
 
+Lemma Zdivide_interval:
+  forall a b c,
+  0 < c -> 0 <= a < b -> (c | a) -> (c | b) -> 0 <= a <= b - c.
+Proof.
+  intros. destruct H1 as [x EQ1]. destruct H2 as [y EQ2]. subst. destruct H0.
+  split. omega. exploit Zmult_lt_reg_r; eauto. intros. 
+  replace (y * c - c) with ((y - 1) * c) by ring.
+  apply Zmult_le_compat_r; omega.
+Qed.
+
 (** Conversion from [Z] to [nat]. *)
 
 Definition nat_of_Z: Z -> nat := Z.to_nat.
@@ -1250,6 +1260,17 @@ Proof.
   intros. unfold proj_sumbool. destruct a. auto. contradiction. 
 Qed.
 
+Ltac InvBooleans :=
+  match goal with
+  | [ H: _ && _ = true |- _ ] =>
+      destruct (andb_prop _ _ H); clear H; InvBooleans
+  | [ H: _ || _ = false |- _ ] =>
+      destruct (orb_false_elim _ _ H); clear H; InvBooleans
+  | [ H: proj_sumbool ?x = true |- _ ] =>
+      generalize (proj_sumbool_true _ H); clear H; intro; InvBooleans
+  | _ => idtac
+  end.
+
 Section DECIDABLE_EQUALITY.
 
 Variable A: Type.
-- 
cgit