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

1 files changed, 4 insertions, 4 deletions

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'));