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

diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index bf1aaf8db..ca4519ee4 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -51,37 +51,37 @@ Hint Unfold seq.
 
 Lemma leb_refl : forall b:bool, leb b b.
 Proof.
-destruct b; simpl in |- *; auto.
+destruct b; simpl; auto.
 Qed.
 Hint Resolve leb_refl.
 
 Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
 Proof.
-unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
+unfold incl; intros s1 s2 E a; elim (E a); auto.
 Qed.
 
 Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1.
 Proof.
-unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
+unfold incl; intros s1 s2 E a; elim (E a); auto.
 Qed.
 
 Lemma seq_refl : forall x:uniset, seq x x.
 Proof.
-destruct x; unfold seq in |- *; auto.
+destruct x; unfold seq; auto.
 Qed.
 Hint Resolve seq_refl.
 
 Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
 Proof.
-unfold seq in |- *.
-destruct x; destruct y; destruct z; simpl in |- *; intros.
+unfold seq.
+destruct x; destruct y; destruct z; simpl; intros.
 rewrite H; auto.
 Qed.
 
 Lemma seq_sym : forall x y:uniset, seq x y -> seq y x.
 Proof.
-unfold seq in |- *.
-destruct x; destruct y; simpl in |- *; auto.
+unfold seq.
+destruct x; destruct y; simpl; auto.
 Qed.
 
 (** uniset union *)
@@ -90,20 +90,20 @@ Definition union (m1 m2:uniset) :=
 
 Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
 Proof.
-unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.
+unfold seq; unfold union; simpl; auto.
 Qed.
 Hint Resolve union_empty_left.
 
 Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
 Proof.
-unfold seq in |- *; unfold union in |- *; simpl in |- *.
+unfold seq; unfold union; simpl.
 intros x a; rewrite (orb_b_false (charac x a)); auto.
 Qed.
 Hint Resolve union_empty_right.
 
 Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
 Proof.
-unfold seq in |- *; unfold charac in |- *; unfold union in |- *.
+unfold seq; unfold charac; unfold union.
 destruct x; destruct y; auto with bool.
 Qed.
 Hint Resolve union_comm.
@@ -111,14 +111,14 @@ Hint Resolve union_comm.
 Lemma union_ass :
  forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
 Proof.
-unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z; auto with bool.
 Qed.
 Hint Resolve union_ass.
 
 Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
 Proof.
-unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
@@ -126,7 +126,7 @@ Hint Resolve seq_left.
 
 Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
 Proof.
-unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.