Kills the useless tactic annotations "in |- *"

 Most of these heavyweight annotations were introduced a long time ago
 by the automatic 7.x -> 8.0 translator

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 14 insertions, 14 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 60bb50cec..8653640d3 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -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/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index b2b15c705..aed7150c8 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -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,7 +65,7 @@ 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 :
@@ -77,7 +77,7 @@ 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'));