7 files changed, 32 insertions, 31 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 2e463120..eb53f061 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Heap.v 13346 2010-07-28 17:17:32Z msozeau $ i*)
 
 (** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
 
@@ -136,45 +136,46 @@ Section defs.
       (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
       (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
       merge_lem l1 l2.
-
+  Require Import Morphisms.
+  
+  Instance: Equivalence (@meq A).
+  Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
+
+  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
+  Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
+  
   Lemma merge :
     forall l1:list A, Sorted leA l1 ->
     forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
   Proof.
-    simple induction 1; intros.
+    fix 1; intros; destruct l1.
     apply merge_exist with l2; auto with datatypes.
-    elim H2; intros.
-    apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes.
+    rename l1 into l.
+    revert l2 H0. fix 1. intros.
+    destruct l2 as [|a0 l0]. 
+    apply merge_exist with (a :: l); simpl; auto with datatypes. 
     elim (leA_dec a a0); intros.
 
     (* 1 (leA a a0) *)
-    cut (merge_lem l (a0 :: l0)); auto using cons_sort with datatypes.
-    intros [l3 l3sorted l3contents Hrec].
-    apply merge_exist with (a :: l3); simpl in |- *;
+    apply Sorted_inv in H. destruct H.
+    destruct (merge l H (a0 :: l0) H0).
+    apply merge_exist with (a :: l1). clear merge merge0.
       auto using cons_sort, cons_leA with datatypes.
-    apply meq_trans with
-      (munion (singletonBag a)
-	(munion (list_contents _ eqA_dec l)
-          (list_contents _ eqA_dec (a0 :: l0)))).
-    apply meq_right; trivial with datatypes.
-    apply meq_sym; apply munion_ass.
-    intros; apply cons_leA.
+    simpl. rewrite m. now rewrite munion_ass. 
+    intros. apply cons_leA. 
     apply (@HdRel_inv _ leA) with l; trivial with datatypes.
 
     (* 2 (leA a0 a) *)
-    elim X0; simpl in |- *; intros.
-    apply merge_exist with (a0 :: l3); simpl in |- *;
+    apply Sorted_inv in H0. destruct H0.
+    destruct (merge0 l0 H0). clear merge merge0.  
+    apply merge_exist with (a0 :: l1); 
       auto using cons_sort, cons_leA with datatypes.
-    apply meq_trans with
-      (munion (singletonBag a0)
-	(munion (munion (singletonBag a) (list_contents _ eqA_dec l))
-          (list_contents _ eqA_dec l0))).
-    apply meq_right; trivial with datatypes.
-    apply munion_perm_left.
-    intros; apply cons_leA; apply HdRel_inv with (l:=l0); trivial with datatypes.
+    simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
+    repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
+    intros. apply cons_leA. 
+    apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
   Qed.
 
-
   (** ** From trees to multisets *)
 
   (** contents of a tree as a multiset *)
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index f52a24b4..e576db2b 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Mergesort.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** A modular implementation of mergesort (the complexity is O(n.log n) in
    the length of the list) *)
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 1388df6a..00a09051 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: PermutEq.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
 
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index f5f91887..e47e2b84 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: PermutSetoid.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 Require Import Omega Relations Multiset SetoidList.
 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index f88c29cb..1e145f57 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Permutation.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*********************************************************************)
 (** ** List permutations as a composition of adjacent transpositions *)
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 7d75d60a..ab399d40 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Sorted.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Made by Hugo Herbelin *)
 
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 85d89441..860e0517 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Sorting.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 Require Export Sorted.
 Require Export Mergesort.