Various algorithmic improvements that reduce compile times (thanks Alexandre Pilkiewicz):

- Lattice: preserve sharing in "combine" operation
- Kildall: use splay heaps (lib/Heaps.v) for node sets
- RTLgen: add a "nop" before loops so that natural enumeration of nodes
  coincides with (reverse) postorder
- Maps: add PTree.map1 operation, use it in RTL and LTL.
- Driver: increase minor heap size


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 6 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index 03966cdd..47c40e3e 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -87,12 +87,6 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     | _, Novalue => x
     | _, _ => Unknown
     end.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
-  Proof.
-    unfold lub, eq; intros.
-    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
-    destruct x; destruct y; auto.
-  Qed.
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
     unfold lub; intros.
@@ -100,6 +94,13 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     apply ge_refl. apply eq_refl.
     destruct x; destruct y; unfold ge; tauto.
   Qed.
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
+  Proof.
+    unfold lub; intros.
+    case (eq_dec x y); intro.
+    apply ge_refl. subst. apply eq_refl.
+    destruct x; destruct y; unfold ge; tauto.
+  Qed.
 End Approx.
 
 Module D := LPMap Approx.