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

8 files changed, 27 insertions, 27 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index f5daa3014..ec0dfeb81 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -41,7 +41,7 @@ Section Wf_Disjoint_Union.
     well_founded leA -> well_founded leB -> well_founded Le_AsB.
   Proof.
     intros.
-    unfold well_founded in |- *.
+    unfold well_founded.
     destruct a as [a| b].
     apply (acc_A_sum a).
     apply (H a).
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index 1c83c4816..73d66c847 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -24,7 +24,7 @@ Section WfInclusion.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
   Proof.
-    unfold well_founded in |- *; auto with sets.
+    unfold well_founded; auto with sets.
   Qed.
 
 End WfInclusion.
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index 27a1c3811..db89cb356 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -31,7 +31,7 @@ Section Inverse_Image.
 
   Theorem wf_inverse_image : well_founded R -> well_founded Rof.
   Proof.
-    red in |- *; intros; apply Acc_inverse_image; auto.
+    red; intros; apply Acc_inverse_image; auto.
   Qed.
 
   Variable F : A -> B -> Prop.
@@ -49,7 +49,7 @@ Section Inverse_Image.
 
   Theorem wf_inverse_rel : well_founded R -> well_founded RoF.
   Proof.
-    red in |- *; constructor; intros.
+    red; constructor; intros.
     case H0; intros.
     apply (Acc_inverse_rel x); auto.
   Qed.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 6d5b663bd..fe2d83250 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -36,11 +36,11 @@ Section Wf_Lexicographic_Exponentiation.
   Proof.
     simple induction x.
     simple induction z.
-    simpl in |- *; intros H.
+    simpl; intros H.
     inversion_clear H.
-    simpl in |- *; intros; apply (Lt_nil A leA).
+    simpl; intros; apply (Lt_nil A leA).
     intros a l HInd.
-    simpl in |- *.
+    simpl.
     intros.
     inversion_clear H.
     apply (Lt_hd A leA); auto with sets.
@@ -54,7 +54,7 @@ Section Wf_Lexicographic_Exponentiation.
       ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z).
   Proof.
     intros x y; generalize x.
-    elim y; simpl in |- *.
+    elim y; simpl.
     right.
     exists x0; auto with sets.
     intros.
@@ -196,7 +196,7 @@ Section Wf_Lexicographic_Exponentiation.
           Descl x0 /\ Descl (l0 ++ Cons x1 Nil)).
 
 
-    simpl in |- *.
+    simpl.
     split.
     generalize (app_inj_tail _ _ _ _ H2); simple induction 1.
     simple induction 1; auto with sets.
@@ -239,7 +239,7 @@ Section Wf_Lexicographic_Exponentiation.
   Proof.
     intros a b x.
     case x.
-    simpl in |- *.
+    simpl.
     simple induction 1.
     intros.
     inversion H1; auto with sets.
@@ -267,7 +267,7 @@ Section Wf_Lexicographic_Exponentiation.
     case x.
     intros; apply (Lt_nil A leA).
 
-    simpl in |- *; intros.
+    simpl; intros.
     inversion_clear H0.
     apply (Lt_hd A leA a b); auto with sets.
 
@@ -284,17 +284,17 @@ Section Wf_Lexicographic_Exponentiation.
     apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).
     auto with sets.
 
-    unfold lex_exp in |- *; simpl in |- *; auto with sets.
+    unfold lex_exp; simpl; auto with sets.
   Qed.
 
 
   Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
   Proof.
-    unfold well_founded at 2 in |- *.
+    unfold well_founded at 2.
     simple induction a; intros x y.
     apply Acc_intro.
     simple induction y0.
-    unfold lex_exp at 1 in |- *; simpl in |- *.
+    unfold lex_exp at 1; simpl.
     apply rev_ind with
       (A := A)
       (P := fun x:List =>
@@ -335,8 +335,8 @@ Section Wf_Lexicographic_Exponentiation.
     intro.
     apply Acc_intro.
     simple induction y2.
-    unfold lex_exp at 1 in |- *.
-    simpl in |- *; intros x4 y3. intros.
+    unfold lex_exp at 1.
+    simpl; intros x4 y3. intros.
     apply (H0 x4 y3); auto with sets.
 
     intros.
@@ -357,7 +357,7 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (HInd2 f); intro.
     apply Acc_intro.
     simple induction y3.
-    unfold lex_exp at 1 in |- *; simpl in |- *; intros.
+    unfold lex_exp at 1; simpl; intros.
     apply H15; auto with sets.
   Qed.
 
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 9a1d66f43..a0c639e4e 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -60,7 +60,7 @@ Section WfLexicographic_Product.
     well_founded leA ->
     (forall x:A, well_founded (leB x)) -> well_founded LexProd.
   Proof.
-    intros wfA wfB; unfold well_founded in |- *.
+    intros wfA wfB; unfold well_founded.
     destruct a.
     apply acc_A_B_lexprod; auto with sets; intros.
     red in wfB.
@@ -94,7 +94,7 @@ Section Wf_Symmetric_Product.
   Lemma wf_symprod :
     well_founded leA -> well_founded leB -> well_founded Symprod.
   Proof.
-    red in |- *.
+    red.
     destruct a.
     apply Acc_symprod; auto with sets.
   Defined.
@@ -161,7 +161,7 @@ Section Swap.
 
   Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
   Proof.
-    red in |- *.
+    red.
     destruct a; intros.
     apply Acc_swapprod; auto with sets.
   Defined.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index e9bc7ccf7..5d06c6c02 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -18,7 +18,7 @@ Section Wf_Transitive_Closure.
   Notation trans_clos := (clos_trans A R).
 
   Lemma incl_clos_trans : inclusion A R trans_clos.
-    red in |- *; auto with sets.
+    red; auto with sets.
   Qed.
 
   Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x.
@@ -39,7 +39,7 @@ Section Wf_Transitive_Closure.
 
   Theorem wf_clos_trans : well_founded R -> well_founded trans_clos.
   Proof.
-    unfold well_founded in |- *; auto with sets.
+    unfold well_founded; auto with sets.
   Defined.
 
 End Wf_Transitive_Closure.
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index e3fdc4c5e..c0aa1c0db 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -51,7 +51,7 @@ Section WfUnion.
 
     elim strip_commut with x x0 y0; auto with sets; intros.
     apply Acc_inv_trans with x1; auto with sets.
-    unfold union in |- *.
+    unfold union.
     elim H11; auto with sets; intros.
     apply t_trans with y1; auto with sets.
 
@@ -65,7 +65,7 @@ Section WfUnion.
   Theorem wf_union :
     commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
   Proof.
-    unfold well_founded in |- *.
+    unfold well_founded.
     intros.
     apply Acc_union; auto with sets.
   Qed.
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index fc4e2ebce..452da1b2e 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -25,7 +25,7 @@ Section WellOrdering.
 
   Theorem wf_WO : well_founded le_WO.
   Proof.
-    unfold well_founded in |- *; intro.
+    unfold well_founded; intro.
     apply Acc_intro.
     elim a.
     intros.
@@ -37,7 +37,7 @@ Section WellOrdering.
     apply (H v0 y0).
     cut (f = f1).
     intros E; rewrite E; auto.
-    symmetry  in |- *.
+    symmetry .
     apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
   Qed.
 
@@ -61,7 +61,7 @@ Section Characterisation_wf_relations.
     apply (well_founded_induction_type H (fun a:A => WO A B)); auto.
     intros x H1.
     apply (sup A B x).
-    unfold B at 1 in |- *.
+    unfold B at 1.
     destruct 1 as [x0].
     apply (H1 x0); auto.
 Qed.