Imported Upstream version 8.4dfsgupstream/8.4dfsg

7 files changed, 23 insertions, 23 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 60bb50ce..8b1bdbd4 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -55,13 +55,13 @@ Section defs.
 
   Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
   Proof.
-    simpl in |- *; auto with datatypes.
+    simpl; auto with datatypes.
   Qed.
 
   Lemma leA_Tree_Node :
     forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
   Proof.
-    simpl in |- *; auto with datatypes.
+    simpl; auto with datatypes.
   Qed.
 
 
@@ -121,7 +121,7 @@ Section defs.
     forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
   Proof.
     simple induction T; auto with datatypes.
-    intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
+    intros; simpl; apply leA_trans with b; auto with datatypes.
   Qed.
 
   (** ** Merging two sorted lists *)
@@ -213,12 +213,12 @@ Section defs.
     simple induction 1; intros.
     apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    simpl in |- *; unfold meq, munion in |- *; auto using node_is_heap with datatypes.
+    simpl; unfold meq, munion; auto using node_is_heap with datatypes.
     elim (leA_dec a a0); intros.
     elim (X a0); intros.
     apply insert_exist with (Tree_Node a T2 T0);
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    simpl in |- *; apply treesort_twist1; trivial with datatypes.
+    simpl; apply treesort_twist1; trivial with datatypes.
     elim (X a); intros T3 HeapT3 ConT3 LeA.
     apply insert_exist with (Tree_Node a0 T2 T3);
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
@@ -226,7 +226,7 @@ Section defs.
     apply low_trans with a; auto with datatypes.
     apply LeA; auto with datatypes.
     apply low_trans with a; auto with datatypes.
-    simpl in |- *; apply treesort_twist2; trivial with datatypes.
+    simpl; apply treesort_twist2; trivial with datatypes.
   Qed.
 
 
@@ -242,10 +242,10 @@ Section defs.
   Proof.
     simple induction l.
     apply (heap_exist nil Tree_Leaf); auto with datatypes.
-    simpl in |- *; unfold meq in |- *; exact nil_is_heap.
+    simpl; unfold meq; exact nil_is_heap.
     simple induction 1.
     intros T i m; elim (insert T i a).
-    intros; apply heap_exist with T1; simpl in |- *; auto with datatypes.
+    intros; apply heap_exist with T1; simpl; auto with datatypes.
     apply meq_trans with (munion (contents T) (singletonBag a)).
     apply meq_trans with (munion (singletonBag a) (contents T)).
     apply meq_right; trivial with datatypes.
@@ -269,7 +269,7 @@ Section defs.
     apply flat_exist with (nil (A:=A)); auto with datatypes.
     elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
     elim (merge _ s1 _ s2); intros.
-    apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
+    apply flat_exist with (a :: l); simpl; auto with datatypes.
     apply meq_trans with
       (munion (list_contents _ eqA_dec l1)
 	(munion (list_contents _ eqA_dec l2) (singletonBag a))).
@@ -288,7 +288,7 @@ Section defs.
     forall l:list A,
     {m : list A | Sorted leA m & permutation _ eqA_dec l m}.
   Proof.
-    intro l; unfold permutation in |- *.
+    intro l; unfold permutation.
     elim (list_to_heap l).
     intros.
     elim (heap_to_list T); auto with datatypes.
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index 7124cd53..301a2142 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -131,7 +131,7 @@ Theorem Sorted_merge : forall l1 l2,
   Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
 Proof.
 induction l1; induction l2; intros; simpl; auto.
-  destruct (a <=? a0) as ()_eqn:Heq1.
+  destruct (a <=? a0) eqn:Heq1.
     invert H.
       simpl. constructor; trivial; rewrite Heq1; constructor.
       assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto).
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index d4e5fba4..cc47b500 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index fa807c15..2cd4f5f7 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -52,7 +52,7 @@ Lemma list_contents_app :
   forall l m:list A,
     meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
 Proof.
-  simple induction l; simpl in |- *; auto with datatypes.
+  simple induction l; simpl; auto with datatypes.
   intros.
   apply meq_trans with
     (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
@@ -65,19 +65,19 @@ Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
 
 Lemma permut_refl : forall l:list A, permutation l l.
 Proof.
-  unfold permutation in |- *; auto with datatypes.
+  unfold permutation; auto with datatypes.
 Qed.
 
 Lemma permut_sym :
   forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
 Proof.
-  unfold permutation, meq; intros; apply sym_eq; trivial.
+  unfold permutation, meq; intros; symmetry; trivial.
 Qed.
 
 Lemma permut_trans :
   forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
 Proof.
-  unfold permutation in |- *; intros.
+  unfold permutation; intros.
   apply meq_trans with (list_contents m); auto with datatypes.
 Qed.
 
@@ -102,7 +102,7 @@ Lemma permut_app :
   forall l l' m m':list A,
     permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
 Proof.
-  unfold permutation in |- *; intros.
+  unfold permutation; intros.
   apply meq_trans with (munion (list_contents l) (list_contents m));
     auto using permut_cons, list_contents_app with datatypes.
   apply meq_trans with (munion (list_contents l') (list_contents m'));
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 797583d0..a69c4aa7 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 0e230b77..03952c95 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 22e56592..ab03cb5e 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)