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, 4 insertions, 4 deletions

diff --git a/backend/CastOptim.v b/backend/CastOptim.v
index 545564d8..19d0065f 100644
--- a/backend/CastOptim.v
+++ b/backend/CastOptim.v
@@ -136,12 +136,12 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     | Single, Single => Single
     | _, _ => Unknown
     end.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
+  Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
-    unfold lub, eq; intros.
-    destruct x; destruct y; auto.
+    unfold lub, ge; intros.
+    destruct x; destruct y; auto. 
   Qed.
-  Lemma ge_lub_left: forall x y, ge (lub x y) x.
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
   Proof.
     unfold lub, ge; intros.
     destruct x; destruct y; auto.