Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

4 files changed, 15 insertions, 12 deletions

diff --git a/lib/Heaps.v b/lib/Heaps.v
index 9fa07a1d..85343998 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -256,14 +256,14 @@ Proof.
   eapply gt_heap_trans with y; eauto. red; auto.
 - intuition.
   eapply lt_heap_trans; eauto. red; auto.
-  eapply gt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto with ordered_type.
 - intuition. eapply gt_heap_trans; eauto. red; auto.
 - rewrite e3 in *; simpl in *. intuition.
   eapply lt_heap_trans with y; eauto. red; auto.
   eapply gt_heap_trans; eauto. red; auto.
 - intuition.
   eapply lt_heap_trans with y; eauto. red; auto.
-  eapply gt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto with ordered_type.
   eapply gt_heap_trans with x; eauto. red; auto.
 - rewrite e3 in *; simpl in *; intuition.
   eapply gt_heap_trans; eauto. red; auto.
@@ -308,7 +308,7 @@ Proof.
   intros. unfold insert.
   case_eq (partition x h). intros a b EQ; simpl.
   assert (E.eq y x \/ ~E.eq y x).
-    destruct (E.compare y x); auto.
+    destruct (E.compare y x); auto with ordered_type.
     right; red; intros. elim (E.lt_not_eq l). apply E.eq_sym; auto.
   destruct H0.
   tauto.
diff --git a/lib/Integers.v b/lib/Integers.v
index 3e78ee60..bc05a4da 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -3327,10 +3327,11 @@ Proof.
   assert (0 <= Z.min (size a) (size b)).
     generalize (size_range a) (size_range b). zify; omega.
   apply bits_size_3. auto. intros.
-  rewrite bits_and. zify. subst z z0. destruct H1.
-  rewrite (bits_size_2 a). auto. omega.
-  rewrite (bits_size_2 b). apply andb_false_r. omega.
-  omega.
+  rewrite bits_and by omega.
+  rewrite andb_false_iff.
+  generalize (bits_size_2 a i).
+  generalize (bits_size_2 b i).
+  zify; intuition.
 Qed.
 
 Corollary and_interval:
diff --git a/lib/IntvSets.v b/lib/IntvSets.v
index 78c20cc5..b97d9882 100644
--- a/lib/IntvSets.v
+++ b/lib/IntvSets.v
@@ -102,7 +102,7 @@ Proof.
   simpl. rewrite IHok. tauto.
   destruct (zlt h0 l).
   simpl. tauto.
-  rewrite IHok. intuition.
+  rewrite IHok. intuition idtac.
   assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto.
   left; xomega.
   left; xomega.
diff --git a/lib/Ordered.v b/lib/Ordered.v
index bcf24cbd..1adbd330 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -21,6 +21,8 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import Integers.
 
+Create HintDb ordered_type.
+
 (** The ordered type of positive numbers *)
 
 Module OrderedPositive <: OrderedType.
@@ -173,17 +175,17 @@ Definition eq (x y: t) :=
 
 Lemma eq_refl : forall x : t, eq x x.
 Proof.
-  intros; split; auto.
+  intros; split; auto with ordered_type.
 Qed.
 
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
 Proof.
-  unfold eq; intros. intuition auto.
+  unfold eq; intros. intuition auto with ordered_type.
 Qed.
 
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
 Proof.
-  unfold eq; intros. intuition eauto.
+  unfold eq; intros. intuition eauto with ordered_type.
 Qed.
 
 Definition lt (x y: t) :=
@@ -201,7 +203,7 @@ Proof.
   case (A.compare (fst x) (fst z)); intro.
   assumption.
   generalize (A.lt_not_eq H2); intro. elim H5.
-  apply A.eq_trans with (fst z). auto. auto.
+  apply A.eq_trans with (fst z). auto. auto with ordered_type.
   generalize (@A.lt_not_eq (fst z) (fst y)); intro.
   elim H5. apply A.lt_trans with (fst x); auto.
   apply A.eq_sym; auto.